third-party/codemirror-3.15/demo/lint.html

   1 <!doctype html>
   2 <html>
   3   <head>
   4     <meta charset="utf-8">
   5     <title>CodeMirror: Linter Demo</title>
   6     <link rel="stylesheet" href="../lib/codemirror.css">
   7     <script src="../lib/codemirror.js"></script>
   8     <script src="../mode/javascript/javascript.js"></script>
   9     <script src="http://ajax.aspnetcdn.com/ajax/jshint/r07/jshint.js"></script>
  10     <script src="https://rawgithub.com/zaach/jsonlint/79b553fb65c192add9066da64043458981b3972b/lib/jsonlint.js"></script>
  11     <link rel="stylesheet" href="../doc/docs.css">
  12     <link rel="stylesheet" href="../addon/lint/lint.css">
  13     <script src="../addon/lint/lint.js"></script>
  14     <script src="../addon/lint/javascript-lint.js"></script>
  15     <script src="../addon/lint/json-lint.js"></script>
  16
  17     <style type="text/css">
  18       .CodeMirror {border: 1px solid black;}
  19     </style>
  20   </head>
  21   <body>
  22     <h1>CodeMirror: Linter Demo</h1>
  23
  24     <p><textarea id="code-js">var widgets = []
  25 function updateHints() {
  26   editor.operation(function(){
  27     for (var i = 0; i < widgets.length; ++i)
  28       editor.removeLineWidget(widgets[i]);
  29     widgets.length = 0;
  30
  31     JSHINT(editor.getValue());
  32     for (var i = 0; i < JSHINT.errors.length; ++i) {
  33       var err = JSHINT.errors[i];
  34       if (!err) continue;
  35       var msg = document.createElement("div");
  36       var icon = msg.appendChild(document.createElement("span"));
  37       icon.innerHTML = "!!";
  38       icon.className = "lint-error-icon";
  39       msg.appendChild(document.createTextNode(err.reason));
  40       msg.className = "lint-error";
  41       widgets.push(editor.addLineWidget(err.line - 1, msg, {coverGutter: false, noHScroll: true}));
  42     }
  43   });
  44   var info = editor.getScrollInfo();
  45   var after = editor.charCoords({line: editor.getCursor().line + 1, ch: 0}, "local").top;
  46   if (info.top + info.clientHeight < after)
  47     editor.scrollTo(null, after - info.clientHeight + 3);
  48 }
  49 </textarea></p>
  50
  51     <p><textarea id="code-json">[
  52  {
  53   _id: "post 1",
  54   "author": "Bob",
  55   "content": "...",
  56   "page_views": 5
  57  },
  58  {
  59   "_id": "post 2",
  60   "author": "Bob",
  61   "content": "...",
  62   "page_views": 9
  63  },
  64  {
  65   "_id": "post 3",
  66   "author": "Bob",
  67   "content": "...",
  68   "page_views": 8
  69  }
  70 ]
  71 </textarea></p>
  72
  73 <script>
  74   var editor = CodeMirror.fromTextArea(document.getElementById("code-js"), {
  75     lineNumbers: true,
  76     mode: "javascript",
  77     gutters: ["CodeMirror-lint-markers"],
  78     lint: true
  79   });
  80
  81   var editor_json = CodeMirror.fromTextArea(document.getElementById("code-json"), {
  82     lineNumbers: true,
  83     mode: "application/json",
  84     gutters: ["CodeMirror-lint-markers"],
  85     lint: true
  86   });
  87 </script>
  88
  89   </body>
  90 </html>