Support multiple formats in TryWhy3 (fix #460).

Makefile.in

@@ -1779,7 +1779,8 @@ src/trywhy3/why3_worker.js: src/trywhy3/why3_worker.byte src/trywhy3/try_alt_erg
 		`find stdlib -name "*.mlw" -printf " --file=%p:/%p"` \
 	+dynlink.js +toplevel.js $<
 
-src/trywhy3/why3_worker.byte: $(WHY3CMA) $(addprefix src/trywhy3/, bindings.cmo worker_proto.cmo why3_worker.cmo)
+src/trywhy3/why3_worker.byte: $(WHY3CMA) lib/plugins/python.cmo lib/plugins/microc.cmo \
+		$(addprefix src/trywhy3/, bindings.cmo worker_proto.cmo why3_worker.cmo)
 	$(JSOCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
 
 src/trywhy3/alt_ergo_worker.js: src/trywhy3/alt_ergo_worker.byte

src/trywhy3/trywhy3.html

@@ -51,6 +51,15 @@
 
 	<div class="why3-separator" style="width:2em;"></div>
 
+	<div class="why3-button-group">
+	  <select  id="why3-select-format"
+		   title="Choose an input format">
+	    <option disabled="disabled" selected="selected">&nbsp;</option>
+	  </select>
+	</div>
+
+	<div class="why3-separator" style="width:2em;"></div>
+
 	<div class="why3-button-group">
 	  <span id="why3-example-label" class="fas fa-spin fa-refresh why3-icon"></span>
 	  <select  id="why3-select-example"

src/trywhy3/why3_worker.ml

@@ -346,13 +346,13 @@ let why3_execute modules =
 
 let () = Sys_js.create_file ~name:temp_file_name ~content:""
 
-let why3_run f lang code =
+let why3_run f format lang code =
   try
     let ch = open_out temp_file_name in
     output_string ch code;
     close_out ch;
 
-    let (theories, _) = Env.read_file lang env temp_file_name in
+    let (theories, _) = Env.read_file ~format lang env temp_file_name in
     W.send (Warning !Task.warnings);
     f theories
   with
@@ -367,27 +367,30 @@ let why3_run f lang code =
 		      "unexpected exception: %a (%s)" Exn_printer.exn_printer e
 		      (Printexc.to_string e)))
 
+let handle_message = function
+  | Transform (`Split, id) -> why3_split id
+  | Transform (`Prove(steps), id) -> why3_prove ~steps id
+  | Transform (`Clean, id) -> why3_clean id
+  | ProveAll -> why3_prove_all ()
+  | ParseBuffer (format, code) ->
+      Task.clear_warnings ();
+      Task.clear_table ();
+      why3_run why3_parse_theories format Env.base_language code
+  | ExecuteBuffer (format, code) ->
+      Task.clear_warnings ();
+      Task.clear_table ();
+      why3_run why3_execute format Pmodule.mlw_language code
+  | SetStatus (st, id) -> List.iter W.send (Task.set_status id st)
+  | GetFormats ->
+      let formats = Env.list_formats Env.base_language in
+      let formats = List.map (fun (name, ext, _) -> (name, ext)) formats in
+      W.send (Formats formats)
+
 
 let () =
-  W.set_onmessage
-    (fun msg ->
-     let () =
-       match msg with
-       | Transform (`Split, id) -> why3_split id
-       | Transform (`Prove(steps), id) -> why3_prove ~steps id
-       | Transform (`Clean, id) -> why3_clean id
-       | ProveAll -> why3_prove_all ()
-       | ParseBuffer code ->
-          Task.clear_warnings ();
-          Task.clear_table ();
-          why3_run why3_parse_theories Env.base_language code
-       | ExecuteBuffer code ->
-          Task.clear_warnings ();
-	  Task.clear_table ();
-	  why3_run why3_execute Pmodule.mlw_language code
-       | SetStatus (st, id) -> List.iter W.send (Task.set_status id st)
-     in
-     W.send Idle
+  W.set_onmessage (fun msg ->
+      handle_message msg;
+      W.send Idle
     )
 (*
 Local Variables:

src/trywhy3/worker_proto.ml

@@ -16,21 +16,25 @@ type loc = int * int * int * int
 type why3_loc = string * (int * int * int) (* kind, line, column, length *)
 type status = [`New | `Valid | `Unknown ]
 
-type why3_command =  ParseBuffer of string
-		   | ExecuteBuffer of string
-		   | ProveAll
-		   | Transform of [ `Prove of int | `Split | `Clean ] * id
-		   | SetStatus of status * id
-
-type why3_output = Error of string (* msg *)
-                 | ErrorLoc of (loc * string) (* loc * msg *)
-                 | Theory of id * string (* Theory (id, name) *)
-                 | Task of (id * id * string * string * why3_loc list * string * int)
-                 (* id, parent id, expl, code, location list, pretty, steps*)
-                 | Result of string list
-                 | UpdateStatus of status * id
-                 | Warning of ((int*int) * string) list
-                 | Idle
+type why3_command =
+  | ParseBuffer of string * string
+  | ExecuteBuffer of string * string
+  | ProveAll
+  | Transform of [ `Prove of int | `Split | `Clean ] * id
+  | SetStatus of status * id
+  | GetFormats
+
+type why3_output =
+  | Error of string (* msg *)
+  | ErrorLoc of (loc * string) (* loc * msg *)
+  | Theory of id * string (* Theory (id, name) *)
+  | Task of (id * id * string * string * why3_loc list * string * int)
+  (* id, parent id, expl, code, location list, pretty, steps*)
+  | Result of string list
+  | UpdateStatus of status * id
+  | Warning of ((int*int) * string) list
+  | Idle
+  | Formats of (string * string list) list
 
 type prover_command = OptionSteps of int | Goal of id * string * int
 type prover_output = Valid | Unknown of string | Invalid of string