Commit 1e761c09 authored by POGODALLA Sylvain's avatar POGODALLA Sylvain

--no commit message

--no commit message
parent 1e455cab
......@@ -451,8 +451,10 @@ struct
let eta_long_form term stype sg =
Lambda.eta_long_form (Lambda.normalize (expand_term term sg)) (expand_type stype sg) (fun id -> get_type_of_const_id id sg)
let unfold t sg = Lambda.normalize (expand_term t sg)
let add_entry e ({size=s} as sg) =
match e with
......@@ -541,6 +543,9 @@ struct
| Term_declaration (s,_,_,_) -> Some s
| _ -> None
end
module Table = Table.Make_table(struct let b = 10 end)
......
......@@ -25,6 +25,7 @@ sig
type env
exception Not_yet_implemented of string
exception Stop
type action =
| Load
......@@ -95,6 +96,7 @@ struct
type entry=E.entry
exception Not_yet_implemented of string
exception Stop
let interactive = ref false
......@@ -103,9 +105,12 @@ struct
module Data_parser = Data_parser.Make(E)
let load t filename dirs e =
match t with
| Data -> Data_parser.parse_data ~override:true filename dirs e
| Script f -> f filename dirs e
try
match t with
| Data -> Data_parser.parse_data ~override:true filename dirs e
| Script f -> f filename dirs e
with
| Stop -> e
let list e =
......
......@@ -25,6 +25,7 @@ sig
type env
exception Not_yet_implemented of string
exception Stop
type action =
| Load
......
......@@ -40,9 +40,8 @@
let global_data = false,true,[""]
let echo ((_:bool),b,(_:string list)) s = if b then Printf.printf "%s\n%!" s else ()
let wait (b,(_:bool),(_:string list)) f = if b then ignore (f ())
let wait (b,(_:bool),(_:string list)) f =
if b then ignore (f () )
}
......@@ -90,8 +89,12 @@
let _ = Script_lexer.reset_echo () in
e
in
let () = wait dyp.global_data read_line in
(e',[Local_data (e',f)])}
try
let () = wait dyp.global_data read_line in
(e',[Local_data (e',f)])
with
| Sys.Break
| End_of_file -> raise F.Stop }
zzcommands @{let e,f = (dyp.last_local_data) in e,[Local_data (e,f)]}
......@@ -233,6 +236,7 @@
try (fst (List.hd (zzcommands ~global_data:(false,verbose,includes) ~local_data:(env,parse_file ~verbose) Script_lexer.lexer lexbuf))) with
| Dyp.Syntax_error -> raise (Error.dyp_error lexbuf "stdin")
with
| F.Stop -> env
| Failure "lexing: empty token" -> env
| Error.Error e ->
let () = Printf.fprintf stderr "Error: %s\n%!" (Error.error_msg e "stdin") in
......
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