Commit c709ab84 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Select highlighting mode depending on format.

parent 8b4b445b
......@@ -1753,7 +1753,10 @@ TRYWHY3_PACK = \
trywhy3.js trywhy3.html trywhy3.css \
README.md examples/ \
trywhy3_custom.css gen_index.sh \
ace-builds/src-min-noconflict/ace.js ace-builds/src-min-noconflict/mode-why3.js \
ace-builds/src-min-noconflict/ace.js \
ace-builds/src-min-noconflict/mode-why3.js \
ace-builds/src-min-noconflict/mode-python.js \
ace-builds/src-min-noconflict/mode-c_cpp.js \
ace-builds/src-min-noconflict/theme-chrome.js $(JS_MAPS)
trywhy3.tar.gz: $(addprefix src/trywhy3/, $(TRYWHY3_PACK))
......
......@@ -56,22 +56,6 @@ Instructions to build TryWhy3
You may want to add a symbolic link from `index.html` to `trywhy3.html` (or rename the file).
To compile with a different file format (e.g. Python, Micro-C)
--------------------------------------------------------------
* In `Makefile.in`, change the line
TRYWHY3CMO=lib/why3/why3.cma
to add the adequate plugin
TRYWHY3CMO=lib/why3/why3.cma lib/plugins/microc.cmo
* In `src/trywhy3/why3_worker.ml`, modify line 354 to specify the format
let (theories, _) = Env.read_file ~format:"micro-C" lang ...
Customization
-------------
......
diff --git a/Makefile.in b/Makefile.in
index e2b417f65..d381e8174 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -1513,7 +1513,7 @@ ALTERGOMODS=util/config util/version util/emap util/myUnix util/myDynlink \
main/frontend
ALTERGOCMO=$(addprefix $(ALTERGODIR)/src/, $(addsuffix .cmo,$(ALTERGOMODS)))
-TRYWHY3CMO=lib/why3/why3.cma
+TRYWHY3CMO=lib/why3/why3.cma lib/plugins/python.cmo
TRYWHY3FILES=trywhy3.js trywhy3.html trywhy3.css \
README examples/ \
trywhy3_custom.css gen_index.sh fontawesome/css/font-awesome.min.css \
@@ -1521,6 +1521,7 @@ TRYWHY3FILES=trywhy3.js trywhy3.html trywhy3.css \
fontawesome/fonts/fontawesome-webfont.woff fontawesome/fonts/fontawesome-webfont.eot \
fontawesome/fonts/fontawesome-webfont.ttf fontawesome/fonts/fontawesome-webfont.woff2 \
ace-builds/src-min-noconflict/ace.js ace-builds/src-min-noconflict/mode-why3.js \
+ ace-builds/src-min-noconflict/mode-python.js \
ace-builds/src-min-noconflict/theme-chrome.js $(JS_MAPS)
trywhy3_package: trywhy3
diff --git a/src/trywhy3/trywhy3.html b/src/trywhy3/trywhy3.html
index b1f85157e..f19a32042 100644
--- a/src/trywhy3/trywhy3.html
+++ b/src/trywhy3/trywhy3.html
@@ -13,7 +13,7 @@
<script type="text/javascript">
var load_embedded_files = false;
var editor_theme = "ace/theme/chrome";
- var editor_mode = "ace/mode/why3";
+ var editor_mode = "ace/mode/python";
var task_viewer_mode = "ace/mode/why3";
var library_index = "examples/index.txt";
</script>
diff --git a/src/trywhy3/why3_worker.ml b/src/trywhy3/why3_worker.ml
index a1e17ac6f..8221c4ff8 100644
--- a/src/trywhy3/why3_worker.ml
+++ b/src/trywhy3/why3_worker.ml
@@ -24,7 +24,7 @@ let () = log_time ("Initialising why3 worker: start ")
(* Name of the pseudo file *)
-let temp_file_name = "/trywhy3_input.mlw"
+let temp_file_name = "/trywhy3_input.py"
(* reads the config file *)
let config : Whyconf.config = Whyconf.read_config (Some why3_conf_file)
......@@ -14,7 +14,6 @@
<script type="text/javascript">
var load_embedded_files = false;
var editor_theme = "ace/theme/chrome";
var editor_mode = "ace/mode/why3";
var task_viewer_mode = "ace/mode/why3";
var library_index = "examples/index.txt";
</script>
......
......@@ -157,11 +157,9 @@ module Editor =
let () =
let editor_theme : Js.js_string Js.t = get_global "editor_theme" in
let editor_mode : Js.js_string Js.t = get_global "editor_mode" in
let task_viewer_mode : Js.js_string Js.t = get_global "task_viewer_mode" in
editor ## setTheme editor_theme;
editor ## getSession ## setMode editor_mode;
JSU.(set editor (Js.string "$blockScrolling") _Infinity);
task_viewer ## setTheme editor_theme;
......@@ -325,13 +323,23 @@ module FormatList = struct
let formats = ref []
let change_mode ext =
let mode =
match ext with
| "py" -> "python"
| "c" -> "c_cpp"
| _ -> "why3" in
let mode = "ace/mode/" ^ mode in
Editor.editor ## getSession ## setMode (Js.string mode)
let handle _ =
let i = select_format ##. selectedIndex in
if i > 0 then
begin match List.nth_opt !formats (i - 1) with
| Some (name, ext :: _) ->
Editor.name := Js.string ("test." ^ ext);
selected_format := name
selected_format := name;
change_mode ext
| Some (name, []) -> selected_format := name
| _ -> selected_format := ""
end;
......@@ -360,7 +368,8 @@ module FormatList = struct
| [] -> ("", 0) in
let (name, idx) = aux 1 !formats in
selected_format := name;
select_format ##. selectedIndex := idx
select_format ##. selectedIndex := idx;
change_mode ext
let add_formats l =
let fresh = !formats = [] in
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment