why3.html 8.87 KB
Newer Older
1 2 3 4 5
<!DOCTYPE html>
<html>
  <head>
    <title>Why3</title>
    <meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
6 7
    <link rel="stylesheet" href="https://use.fontawesome.com/releases/v5.0.13/css/solid.css" integrity="sha384-Rw5qeepMFvJVEZdSo1nDQD5B6wX0m7c5Z/pLNvjkB14W6Yki1hKbSEQaX9ffUbWe" crossorigin="anonymous">
    <link rel="stylesheet" href="https://use.fontawesome.com/releases/v5.0.13/css/fontawesome.css" integrity="sha384-GVa9GOgVQgOk+TNYXu7S/InPTfSDTtBalSgkgqQ7sCik56N9ztlkoTr2f/T44oKV" crossorigin="anonymous">
8 9 10 11 12 13 14 15 16 17 18 19 20
    <link rel="stylesheet" type="text/css" href="why3.css" />
    <link rel="stylesheet" type="text/css" href="why3_custom.css"/>

    <script defer="defer" src="ace-builds/src-min-noconflict/ace.js"
            type="text/javascript" charset="utf-8"></script>

    <script type="text/javascript">
      var load_embedded_files = false;
      var editor_theme = "ace/theme/chrome";
      var editor_mode = "ace/mode/why3";
      var library_index = "examples/index.txt";
    </script>
    <script defer="defer" type="text/javascript"
21
            src="why3_js.js"></script>
22 23 24 25 26 27 28 29 30
  </head>
  <body>
    <div id="why3-main-container" class="why3-container">
      <div id="why3-top-button-bar" class="why3-widget why3-button-bar">

	<div class="why3-separator" style="width:0.1em;"></div>
 	<div class="why3-button-group">
	  <button id="why3-button-open"  class="why3-button"
                  title="Open file (ctrl-o)">
31
	    <span class="fas fa-folder-open"></span>
32 33 34
	  </button>
	  <button id="why3-button-save"  class="why3-button"
                  title="Save file (ctrl-s)">
35
	    <span class="fas fa-save"></span>
36 37 38 39 40 41 42
	  </button>
 	</div>

	<div class="why3-separator" style="width:2em;"></div>
 	<div class="why3-button-group">
	  <button id="why3-button-undo"  class="why3-button"
                  title="Undo edit (ctrl-z)">
43
	    <span class="fas fa-undo"></span>
44 45 46
	  </button>
	  <button id="why3-button-redo"  class="why3-button"
                  title="Repeat edit (ctrl-y)">
47
	    <span class="fas fa-redo"></span>
48 49 50 51 52 53
	  </button>
 	</div>

	<div class="why3-separator" style="width:2em;"></div>

	<div class="why3-button-group">
54
	  <span id="why3-example-label" class="fas fa-refresh why3-icon"></span>
55 56 57 58 59 60 61 62 63 64
	  <select  id="why3-select-example"
		   title="Choose a predefined example">
	    <option disabled="disabled" selected="selected">&nbsp;</option>
	  </select>
	</div>

	<div class="why3-separator" style="width:2em;"></div>

	<div class="why3-button-group">
          <button id="why3-button-compile" class="why3-button" title="Compile buffer">
65
	    <span class="fas fa-cogs"></span>
66 67
	  </button>
	  <button id="why3-button-execute" class="why3-button" title="Execute buffer">
68
	    <span class="fas fa-arrow-circle-right"></span>
69 70
	  </button>
	  <button id="why3-button-stop" class="why3-button" title="Interrupt">
71
	    <span class="fas fa-ban"></span>
72 73 74 75 76 77
	  </button>
	</div>

	<div class="why3-button-group why3-flushright">
	  <button id="why3-button-settings" class="why3-button"
		  title="Settings…">
78
	    <span class="fas fa-wrench"></span>
79 80 81
	  </button>
	  <button id="why3-button-help" class="why3-button"
		  title="Help">
82
	    <span class="fas fa-question-circle"></span>
83 84 85
	  </button>
	  <button id="why3-button-about" class="why3-button"
		  title="About">
86
	    <span class="fas fa-info-circle"></span>
87 88 89 90 91 92
	  </button>
	</div>


      </div>

93
      <div id="why3-main-panel">
94

95 96 97
	<div id="why3-task-list-container">
          <div id="why3-task-list">
            Task tree not loaded yet. You may need to click on the 'reload' button (counterclockwise circular arrow above)
98 99 100 101 102
          </div>
        </div>

	<div id="why3-resize-bar" class="why3-widget" ></div>

103 104 105 106 107 108 109
        <div id="why3-right-panel">

	  <div id="why3-tab-container" class="why3-container">
	    <div id="why3-tab-panel" class="why3-tab-group">
	      <span class="why3-tab-label why3-widget" >Task</span>
	      <div class="why3-widget why3-tab">
                <div id="why3-task-viewer"> No current proof task yet</div>
110
	      </div>
111 112 113 114 115
	      <span class="why3-tab-label why3-widget why3-inactive">Source code</span>
	      <div class="why3-widget why3-tab">
	        <div id="why3-editor-container" class="why3-container">
                  <div id="why3-editor">No source code loaded yet</div>
	        </div>
116
              </div>
117 118 119 120 121 122 123 124
	      <span class="why3-tab-label why3-widget why3-inactive">Log</span>
	      <div class="why3-widget why3-tab">
                <div id="why3-log-container" class="why3-container">
                  <div id="why3-log-bg" class="why3-widget">
                    Log</div>
                </div>
              </div>
	    </div>
125 126
	  </div>

127 128 129 130 131
          <!--
              <div id="why3-task-viewer-container" class="why3-container">
                <div id="why3-viewer-bg" class="why3-widget"> </div>
	      </div>
              -->
132 133


134
<!-- TODO remove useless attribute inside why3-form -->
135

136 137
      <div id="why3-resize-bar2" class="why3-widget" ></div>

138
<!-- TODO saisie -->
139
      <div id="why3-form-cont">
140
        <form id="why3-form" method="get"
141 142 143 144
              enctype="plain/text"
              action="http://localho" target="form-answer">
          <input type="text" name="command">
          <input type="submit" name="Submit" class="why3-hidden">
145 146 147
        </form>
      </div>

Sylvain Dailler's avatar
Sylvain Dailler committed
148 149 150 151 152 153 154 155 156 157
      <div id="why3-tab-container2">
	<div id="why3-tab-panel2">
          <span class="why3-widget"></span>
          <div class="why3-widget">
	    <div id="why3-editor-container2">
              <div id="why3-error-container" class="why3-widget">Error message</div>
	    </div>
          </div>
        </div>
      </div>
158

159 160
        </div>
      </div>
161
    </div>
Sylvain Dailler's avatar
Sylvain Dailler committed
162

163 164 165 166 167 168
    <!-- open and save -->
    <a id="why3-save-as" href="" class="why3-hidden"></a>
    <input id="why3-open" type="file" class="why3-hidden" />
    <!-- context menu -->
    <div class="why3-contextmenu why3-widget" id="why3-task-menu">
      <ul>
169
	<li id="why3-split-menu-entry"><span class="fas fa-share-alt
170
						    why3-icon"></span> Split and prove </li>
171
	<li id="why3-prove-menu-entry"><span class="fas fa-check-square
172 173
						    why3-icon"></span>
						    Prove (default) </li>
174
	<li id="why3-prove100-menu-entry"><span class="fas fa-check-square
175 176 177
						    why3-icon"></span>
						    Prove (100
	  steps) </li>
178
	<li id="why3-prove1000-menu-entry"><span class="fas fa-check-square
179 180
							why3-icon"></span>
	  Prove (1000 steps) </li>
181
	<li id="why3-clean-menu-entry"><span class="fas fa-unlink why3-icon"></span>
182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216
	  Clean </li>
      </ul>
    </div>
    <!-- dialogs -->
    <div id="why3-dialog-panel" class="why3-container" >
      <div id="why3-dialog-bg" class="why3-widget"> </div>
      <div class="why3-widget why3-dialog">
	<div id="why3-setting-dialog" class="why3-widget" >
	  <span>Preferences</span>
	  <ul>
            <li>
              <input id="why3-radio-wide" type="radio" name="why3-view"
		     checked="checked" value="wide" />
              <label for="why3-radio-wide">Split Vertically</label>
	    </li>
	    <li>
	      <input id="why3-radio-column" type="radio"
		     name="why3-view" value="column" />
	      <label for="why3-radio-column">Split Horizontally</label>
            </li>
            <li>
              <input id="why3-input-num-threads" type="number" style="width:4em;" min="1" max="8"
                     value="4" /> Number of threads for Alt-Ergo
            </li>
            <li>
              <input id="why3-input-num-steps" type="number" style="width:4em;" min="1" max="1000"
                     value="100" /> Number of steps for Alt-Ergo
            </li>
	  </ul>
	</div>
	<div id="why3-about-dialog" class="why3-widget">
	  <span>About TryWhy3</span>
	  <p>TryWhy3 is a Javascript based version of
	    the <a href="http://why3.lri.fr/" target="_blank">Why3
	    Verification Platform</a></p>
217
	  <p>© 2010-2017,   Inria - CNRS - Paris-Sud University<br/>
218 219 220
	    This software is distributed under the terms of the GNU Lesser
	    General Public License version 2.1, with the special exception
	    on linking described in the
221
	    file <a href="https://gitlab.inria.fr/why3/why3/raw/master/LICENSE"
222 223 224 225 226 227 228 229 230 231 232 233 234 235
	            target="_blank">LICENSE</a>.
	  </p>
	  <p>TryWhy3 relies on the following excellent open source
	    software and resources:
	  </p>
	  <ul>
	    <li>A Javascript version of
	    the <a href="https://alt-ergo.ocamlpro.com/"  target="_blank">Alt-Ergo SMT
		Solver</a>.</li>
	    <li>The <a href="http://ocsigen.org/js_of_ocaml/"  target="_blank">js_of_ocaml</a>
	      OCaml to Javascript compiler, part of
	    the <a href="http://ocsigen.org/"  target="_blank">Ocsigen</a>
	      project.</li>

236
	    <li>The <a href="https://fontawesome.com/"
237 238 239 240 241 242 243 244
		 target="_blank">Font
		Awesome</a> font and CSS toolkit.</li>
	    <li>The <a href="https://ace.c9.io/"  target="_blank">ACE</a> Web editor.</li>
	  </ul>
	</div>
	<button id="why3-close-dialog-button"
		style="float:right;"
		class="why3-button"
245
		title="Close"><span class="fas fa-times"></span></button>
246 247 248 249 250
      </div>
    </div>
  </body>

</html>