) status projections
(* to avoid a long list of recursive functions *)
-let eval_from_stream_greedy_ref = ref (fun _ _ _ -> assert false);;
+let eval_from_stream_ref = ref (fun _ _ _ -> assert false);;
let eval_command status cmd =
match cmd with
+ | TacticAst.Default (loc, what, uris) as cmd ->
+ LibraryObjects.set_default what uris;
+ {status with moo_content_rev =
+ (TacticAstPp.pp_command cmd ^ "\n") :: status.moo_content_rev}
| TacticAst.Include (loc, path) ->
let path = MatitaMisc.obj_file_of_script path in
let stream = Stream.of_channel (open_in path) in
let status = ref status in
- (try
- !eval_from_stream_greedy_ref status stream (fun _ _ -> ())
- with
- CicTextualParser2.Parse_error (floc,err) as exc ->
- (* check for EOI *)
- if Stream.peek stream = None then ()
- else raise exc
- );
+ !eval_from_stream_ref status stream (fun _ _ -> ());
!status
| TacticAst.Set (loc, name, value) ->
let value =
let obj = Cic.Constant (name,Some bo,ty,[],[]) in
MatitaSync.add_obj uri obj status
| TacticAst.Coercion (loc, coercion) ->
- eval_coercion status coercion
+ let status = eval_coercion status coercion in
+ let moo_content_rev =
+ (TacticAstPp.pp_cic_command
+ (TacticAst.Coercion (CicAst.dummy_floc,coercion)) ^ ".\n") ::
+ status.moo_content_rev in
+ {status with moo_content_rev = moo_content_rev}
| TacticAst.Alias (loc, spec) ->
let aliases =
match spec with
status, tacticals
let disambiguate_command status = function
- | TacticAst.Include (loc,path) as cmd -> status,cmd
+ | TacticAst.Default _
+ | TacticAst.Alias _
+ | TacticAst.Include _ as cmd -> status,cmd
| TacticAst.Coercion (loc, term) ->
let status, term = disambiguate_term status term in
status, TacticAst.Coercion (loc,term)
| (TacticAst.Set _ | TacticAst.Qed _ | TacticAst.Drop _ ) as cmd ->
status, cmd
- | TacticAst.Alias _ as x -> status, x
| TacticAst.Obj (loc,obj) ->
let status,obj = disambiguate_obj status obj in
status, TacticAst.Obj (loc,obj)
let stl = CicTextualParser2.parse_statements str in
List.iter
(fun ast -> cb !status ast;status := eval_ast !status ast) stl
+;;
+(* to avoid a long list of recursive functions *)
+eval_from_stream_ref := eval_from_stream;;
+
let eval_from_stream_greedy status str cb =
while true do
print_string "matita> ";
done
;;
-(* to avoid a long list of recursive functions *)
-eval_from_stream_greedy_ref := eval_from_stream_greedy;;
-
let eval_string status str =
eval_from_stream status (Stream.of_string str) (fun _ _ -> ())