| 2004 | } |
| 2005 | } |
| 2006 | function makePrompt(prefix, desc) { |
| 2007 | var raw = ''; |
| 2008 | if (prefix) { |
| 2009 | raw += '<span style="font-family: monospace">' + prefix + '</span>'; |
| 2010 | } |
| 2011 | raw += '<input type="text"/> ' + |
| 2012 | '<span style="color: #888">'; |
| 2013 | if (desc) { |
| 2014 | raw += '<span style="color: #888">'; |
| 2015 | raw += desc; |
| 2016 | raw += '</span>'; |
| 2017 | } |
| 2018 | return raw; |
| 2019 | } |
| 2020 | var searchPromptDesc = '(Javascript regexp)'; |
| 2021 | function showPrompt(cm, onPromptClose, prefix, desc, initialValue) { |
| 2022 | var shortText = (prefix || '') + ' ' + (desc || ''); |