Commit 4737eb90 authored by MARCHE Claude's avatar MARCHE Claude

Try why3: fix order of lemmas and functions in a theory

parent 32a60ef7
......@@ -161,6 +161,7 @@ pvsbin/
/lib/isabelle/Why3_Number.thy
/lib/isabelle/why3.ML
/lib/isabelle/last_build
/lib/isabelle/bv
# /src/driver/
/src/driver/driver_lexer.ml
......
......@@ -132,7 +132,7 @@ let why3_prove theories =
Stdlib.Mstr.fold
(fun thname th acc ->
let tasks = Task.split_theory th None None in
let tasks = List.map
let tasks = List.rev_map
(fun t ->
let (id,expl,_) = Termcode.goal_expl_task ~root:true t in
let expl = match expl with
......@@ -278,10 +278,12 @@ let add_why3_cmd buttonname f input_lang =
(fun _ev ->
let global = Js.Unsafe.global in
let editor = Js.Unsafe.get global (Js.string "editor") in
let lang =
let lang = "en"
(*
Js.to_string
(Js.Unsafe.meth_call editor "getAttribute"
[| Js.Unsafe.inject (Js.string "lang") |])
*)
in
let code = Js.to_string (Js.Unsafe.meth_call editor "getValue" [| |]) in
log ("Why3 is running, lang = " ^ lang);
......
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