Commit 65b7a967 authored by Adrien KOUTSOS's avatar Adrien KOUTSOS

minor indentation

parent 58ab8b20
......@@ -1748,36 +1748,35 @@ let rec exec_cmd_list l state sk fk = match l with
(exec_cmd_list tail)
sk fk c
let rec interactive_loop state sk fk =
let rec interactive_loop state sk fk =
let state = simplify ~collect:true state
|> new_screen in
let state = simplify ~collect:true state
|> new_screen in
(* We set the current proof node to be a User node, to allow backtracking
to it. *)
set_user_node state.c_proof;
(* We set the current proof node to be a User node, to allow backtracking
to it. *)
set_user_node state.c_proof;
Printf.printf "> %!";
let input_string =
if state.param.shell_mode then
get_user_input state
else
try input_line state.param.input_channel with
| End_of_file -> raise Proof_failed in
let (state,input_commands) =
try (state, parse_input input_string) with
| Term_badly_formed s ->
( add_error
(Printf.sprintf "This term is badly formed: %s" s) state,
[] ) in
(* We insert a back_track point here. *)
exec_cmd_list input_commands state
(fun state fk' ->
interactive_loop state sk fk')
(fun () -> interactive_loop state sk fk)
Printf.printf "> %!";
let input_string =
if state.param.shell_mode then
get_user_input state
else
try input_line state.param.input_channel with
| End_of_file -> raise Proof_failed in
let (state,input_commands) =
try (state, parse_input input_string) with
| Term_badly_formed s ->
( add_error
(Printf.sprintf "This term is badly formed: %s" s) state,
[] ) in
(* We insert a back_track point here. *)
exec_cmd_list input_commands state
(fun state fk' ->
interactive_loop state sk fk')
(fun () -> interactive_loop state sk fk)
let rec interactive_proof state_list = match state_list with
......
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