| 123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106 | 
							- <!doctype html>
 
- <html>
 
-   <head>
 
-     <title>CodeMirror 2: Search/Replace Demo</title>
 
-     <link rel="stylesheet" href="../lib/codemirror.css">
 
-     <script src="../lib/codemirror.js"></script>
 
-     <link rel="stylesheet" href="../theme/default.css">
 
-     <script src="../mode/xml/xml.js"></script>
 
-     <link rel="stylesheet" href="../css/docs.css">
 
-     <style type="text/css">
 
-       .CodeMirror {border-top: 1px solid black; border-bottom: 1px solid black;}
 
-       .searched {background: yellow;}
 
-     </style>
 
-   </head>
 
-   <body>
 
-     <h1>CodeMirror 2: Search/Replace Demo</h1>
 
-     <form><textarea id="code" name="code">
 
-   <dt id="option_indentWithTabs"><code>indentWithTabs (boolean)</code></dt>
 
-   <dd>Whether, when indenting, the first N*8 spaces should be
 
-   replaced by N tabs. Default is false.</dd>
 
-   <dt id="option_tabMode"><code>tabMode (string)</code></dt>
 
-   <dd>Determines what happens when the user presses the tab key.
 
-   Must be one of the following:
 
-     <dl>
 
-       <dt><code>"classic" (the default)</code></dt>
 
-       <dd>When nothing is selected, insert a tab. Otherwise,
 
-       behave like the <code>"shift"</code> mode. (When shift is
 
-       held, this behaves like the <code>"indent"</code> mode.)</dd>
 
-       <dt><code>"shift"</code></dt>
 
-       <dd>Indent all selected lines by
 
-       one <a href="#option_indentUnit"><code>indentUnit</code></a>.
 
-       If shift was held while pressing tab, un-indent all selected
 
-       lines one unit.</dd>
 
-       <dt><code>"indent"</code></dt>
 
-       <dd>Indent the line the 'correctly', based on its syntactic
 
-       context. Only works if the
 
-       mode <a href="#indent">supports</a> it.</dd>
 
-       <dt><code>"default"</code></dt>
 
-       <dd>Do not capture tab presses, let the browser apply its
 
-       default behaviour (which usually means it skips to the next
 
-       control).</dd>
 
-     </dl></dd>
 
-   <dt id="option_enterMode"><code>enterMode (string)</code></dt>
 
-   <dd>Determines whether and how new lines are indented when the
 
-   enter key is pressed. The following modes are supported:
 
-     <dl>
 
-       <dt><code>"indent" (the default)</code></dt>
 
-       <dd>Use the mode's indentation rules to give the new line
 
-       the correct indentation.</dd>
 
-       <dt><code>"keep"</code></dt>
 
-       <dd>Indent the line the same as the previous line.</dd>
 
-       <dt><code>"flat"</code></dt>
 
-       <dd>Do not indent the new line.</dd>
 
-     </dl></dd>
 
- </textarea></form>
 
- <button type=button onclick="search()">Search</button>
 
- <input type=text style="width: 5em" id=query value=indent> or
 
- <button type=button onclick="replace()">replace</button> it by
 
- <input type=text style="width: 5em" id=replace>
 
-     <script>
 
- var editor = CodeMirror.fromTextArea(document.getElementById("code"), {mode: "text/html", lineNumbers: true});
 
- var lastPos = null, lastQuery = null, marked = [];
 
- function unmark() {
 
-   for (var i = 0; i < marked.length; ++i) marked[i]();
 
-   marked.length = 0;
 
- }
 
- function search() {
 
-   unmark();                     
 
-   var text = document.getElementById("query").value;
 
-   if (!text) return;
 
-   for (var cursor = editor.getSearchCursor(text); cursor.findNext();)
 
-     marked.push(editor.markText(cursor.from(), cursor.to(), "searched"));
 
-   if (lastQuery != text) lastPos = null;
 
-   var cursor = editor.getSearchCursor(text, lastPos || editor.getCursor());
 
-   if (!cursor.findNext()) {
 
-     cursor = editor.getSearchCursor(text);
 
-     if (!cursor.findNext()) return;
 
-   }
 
-   editor.setSelection(cursor.from(), cursor.to());
 
-   lastQuery = text; lastPos = cursor.to();
 
- }
 
- function replace() {
 
-   unmark();
 
-   var text = document.getElementById("query").value,
 
-       replace = document.getElementById("replace").value;
 
-   if (!text) return;
 
-   for (var cursor = editor.getSearchCursor(text); cursor.findNext();)
 
-     cursor.replace(replace);
 
- }
 
- </script>
 
-     <p>Demonstration of search/replace functionality and marking
 
-     text.</p>
 
-   </body>
 
- </html>
 
 
  |