removed no longer used METAs

[helm.git] / helm / matita / matitaEngine.ml

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index fa9292c8986a7e7033d48c96f27f755b65c46830..f0d8ee46c7820b34feff186135edcd418b9b4fd4 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -23,33 +23,44 @@
  * http://helm.cs.unibo.it/
  *)
 
+(* $Id$ *)
+
 open Printf
 
 let debug = false ;;
 let debug_print = if debug then prerr_endline else ignore ;;
 
-let disambiguate_command lexicon_status_ref status cmd =
+let disambiguate_tactic lexicon_status_ref grafite_status goal tac =
+ let metasenv,tac =
+  GrafiteDisambiguate.disambiguate_tactic
+   lexicon_status_ref
+   (GrafiteTypes.get_proof_context grafite_status goal)
+   (GrafiteTypes.get_proof_metasenv grafite_status)
+   tac
+ in
+  GrafiteTypes.set_metasenv metasenv grafite_status,tac
+
+let disambiguate_command lexicon_status_ref grafite_status cmd =
  let lexicon_status,metasenv,cmd =
   GrafiteDisambiguate.disambiguate_command
    ~baseuri:(
      try
-      Some (GrafiteTypes.get_string_option status "baseuri")
+      Some (GrafiteTypes.get_string_option grafite_status "baseuri")
      with
       GrafiteTypes.Option_error _ -> None)
-   !lexicon_status_ref (GrafiteTypes.get_proof_metasenv status) cmd
+   !lexicon_status_ref (GrafiteTypes.get_proof_metasenv grafite_status) cmd
  in
   lexicon_status_ref := lexicon_status;
-  GrafiteTypes.set_metasenv metasenv status,cmd
+  GrafiteTypes.set_metasenv metasenv grafite_status,cmd
 
-let disambiguate_tactic lexicon_status_ref status goal tac =
- let metasenv,tac =
-  GrafiteDisambiguate.disambiguate_tactic
+let disambiguate_macro lexicon_status_ref grafite_status macro context =
+ let metasenv,macro =
+  GrafiteDisambiguate.disambiguate_macro
    lexicon_status_ref
-   (GrafiteTypes.get_proof_context status goal)
-   (GrafiteTypes.get_proof_metasenv status)
-   tac
+   (GrafiteTypes.get_proof_metasenv grafite_status)
+   context macro
  in
-  GrafiteTypes.set_metasenv metasenv status,tac
+  GrafiteTypes.set_metasenv metasenv grafite_status,macro
 
 let eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status
  grafite_status ast
@@ -59,6 +70,7 @@ let eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status
   GrafiteEngine.eval_ast
    ~disambiguate_tactic:(disambiguate_tactic lexicon_status_ref)
    ~disambiguate_command:(disambiguate_command lexicon_status_ref)
+   ~disambiguate_macro:(disambiguate_macro lexicon_status_ref)
    ?do_heavy_checks ?clean_baseuri grafite_status ast in
  let new_lexicon_status =
   LexiconSync.add_aliases_for_objs !lexicon_status_ref new_objs in
@@ -86,10 +98,16 @@ let eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status
  in
   ((new_grafite_status,new_lexicon_status),None)::intermediate_states
 
-let eval_from_stream ~include_paths ?(prompt=false) ?do_heavy_checks
- ?clean_baseuri lexicon_status grafite_status str cb 
+let eval_from_stream ~first_statement_only ~include_paths ?(prompt=false)
+ ?do_heavy_checks ?clean_baseuri lexicon_status grafite_status str cb 
 =
  let rec loop lexicon_status grafite_status statuses =
+  let loop =
+   if first_statement_only then
+    fun _ _ _ -> raise End_of_file
+   else
+    loop
+  in
    if prompt then (print_string "matita> "; flush stdout);
    try
     let lexicon_status,ast =
@@ -116,8 +134,9 @@ let eval_from_stream ~include_paths ?(prompt=false) ?do_heavy_checks
   loop lexicon_status grafite_status []
 ;;
 
-let eval_string ~include_paths ?do_heavy_checks ?clean_baseuri lexicon_status
- status str
+let eval_string ~first_statement_only ~include_paths ?do_heavy_checks
+ ?clean_baseuri lexicon_status status str
 =
- eval_from_stream ~include_paths ?do_heavy_checks ?clean_baseuri lexicon_status
-  status (Ulexing.from_utf8_string str) (fun _ _ -> ())
+ eval_from_stream ~first_statement_only ~include_paths ?do_heavy_checks
+  ?clean_baseuri lexicon_status status (Ulexing.from_utf8_string str)
+  (fun _ _ -> ())