Commit 58ab8b20 authored by Adrien KOUTSOS's avatar Adrien KOUTSOS

interactive proofs done using success and failure continuations

parent b4e3f2ea
Pipeline #1651 passed with stage
in 3 minutes and 10 seconds
This diff is collapsed.
......@@ -102,7 +102,8 @@ let main_interactive () =
back_track = Root;
node_type = User })
formula_list in
ignore(interactive_proof (State.new_state param proof_list));;
interactive_proof (List.map (State.new_state param) proof_list);;
(**********************)
......
......@@ -10,7 +10,6 @@ open Proof
- param: The parameters of the interactive loop state. *)
type state =
{ mutable c_proof : proof;
mutable danglings : proof list;
mutable input_history : string list;
error_message : unit -> unit;
l_error_ref : int list;
......@@ -32,20 +31,17 @@ let dummy_state () =
node_type = Internal } in
{ c_proof = dummy_proof;
danglings = [];
input_history = [];
error_message = (fun () -> ());
l_error_ref = [];
param = Param.new_emacs_param true }
let new_state param proof_list = match proof_list with
| [] -> failwith "Nothing to prove\n"
| proof :: rem_proof -> { c_proof = proof;
danglings = rem_proof;
input_history = [];
error_message = (fun () -> ());
l_error_ref = [];
param = param }
let new_state param proof =
{ c_proof = proof;
input_history = [];
error_message = (fun () -> ());
l_error_ref = [];
param = param }
(* Add a new error message. *)
......
......@@ -18,7 +18,6 @@ open Side
- param: The parameters of the interactive loop state. *)
type state =
{ mutable c_proof : proof;
mutable danglings : proof list;
mutable input_history : string list;
error_message : unit -> unit;
l_error_ref : int list;
......@@ -31,7 +30,7 @@ type state =
val dummy_state : unit -> state
val new_state : Param.param -> proof list -> state
val new_state : Param.param -> proof -> state
val add_error : string -> state -> state
......
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