Commit 09db98a3 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Try Why3: Tree view of goals

parent 907c910f
...@@ -163,23 +163,33 @@ let run textbox preview (_ : D.mouseEvent Js.t) : bool Js.t = ...@@ -163,23 +163,33 @@ let run textbox preview (_ : D.mouseEvent Js.t) : bool Js.t =
Stdlib.Mstr.fold Stdlib.Mstr.fold
(fun thname th acc -> (fun thname th acc ->
let tasks = Task.split_theory th None None in let tasks = Task.split_theory th None None in
let tasks = List.fold_left let tasks = List.map
(fun acc t -> (fun t ->
let (id,expl,_) = Termcode.goal_expl_task ~root:true t in
let expl = match expl with
| Some s -> s
| None -> id.Ident.id_string
in
let tl = Trans.apply split_trans t in let tl = Trans.apply split_trans t in
List.rev_append tl acc) let tasks =
[] tasks List.map
in (fun task ->
let tasks = let (id,expl,_) = Termcode.goal_expl_task ~root:false task in
List.rev_map let expl = match expl with
(fun task -> | Some s -> s
let (id,expl,_) = Termcode.goal_expl_task ~root:false task in | None -> id.Ident.id_string
let expl = match expl with in
| Some s -> s let result = run_alt_ergo_on_task task in
| None -> id.Ident.id_string let result =
in if String.length result > 80 then
let result = run_alt_ergo_on_task task in "..." ^ String.sub result (String.length result - 80) 80
[Html.of_string (expl ^" : " ^ result)]) else result
tasks in
[Html.of_string (expl ^" : " ^ result)])
tl
in
[Html.of_string expl; Html.ul tasks])
tasks
in in
[ Html.of_string ("Theory " ^ thname); Html.ul tasks] [ Html.of_string ("Theory " ^ thname); Html.ul tasks]
:: acc) :: acc)
......
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