Class mathViewer got rid of. The circular dependency between

[helm.git] / matita / components / grafite_engine / grafiteEngine.ml

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index 79391193dd1f0699de8913b03cd136e0903aff28..c271448a7564b25319a2a841ffbcd436f86c7f98 100644 (file)
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -41,8 +41,12 @@ let basic_eval_unification_hint (t,n) status =
 let inject_unification_hint =
  let basic_eval_unification_hint (t,n) 
    ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
+   ~alias_only status
  =
-  let t = refresh_uri_in_term t in basic_eval_unification_hint (t,n)
+  if not alias_only then
+   let t = refresh_uri_in_term t in basic_eval_unification_hint (t,n) status
+  else
+   status
  in
   GrafiteTypes.Serializer.register#run "unification_hints"
    basic_eval_unification_hint
@@ -54,9 +58,7 @@ let eval_unification_hint status t n =
  assert (metasenv=[]);
  let t = NCicUntrusted.apply_subst subst [] t in
  let status = basic_eval_unification_hint (t,n) status in
- let dump = inject_unification_hint (t,n)::status#dump in
- let status = status#set_dump dump in
-  status
+  NCicLibrary.dump_obj status (inject_unification_hint (t,n))
 ;;
 
 let basic_index_obj l status =
@@ -69,9 +71,12 @@ let basic_index_obj l status =
     status#auto_cache l) 
 ;;     
 
-let basic_eval_interpretation (dsc, (symbol, args), cic_appl_pattern) status =
+let basic_eval_interpretation ~alias_only (dsc, (symbol, args), cic_appl_pattern) status =
  let status =
-  Interpretations.add_interpretation status dsc (symbol, args) cic_appl_pattern
+  if not alias_only then
+   Interpretations.add_interpretation status dsc (symbol, args) cic_appl_pattern
+  else
+   status
  in
  let mode = GrafiteAst.WithPreferences (*assert false*) in (* MATITA 1.0 VEDI SOTTO *)
  let diff =
@@ -83,6 +88,7 @@ let basic_eval_interpretation (dsc, (symbol, args), cic_appl_pattern) status =
 let inject_interpretation =
  let basic_eval_interpretation (dsc, (symbol, args), cic_appl_pattern)
    ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
+   ~alias_only
  =
   let rec refresh =
    function
@@ -94,16 +100,15 @@ let inject_interpretation =
     | NotationPt.ApplPattern l -> NotationPt.ApplPattern (List.map refresh l)
   in
   let cic_appl_pattern = refresh cic_appl_pattern in
-   basic_eval_interpretation (dsc, (symbol, args), cic_appl_pattern)
+   basic_eval_interpretation ~alias_only (dsc, (symbol, args), cic_appl_pattern)
  in
   GrafiteTypes.Serializer.register#run "interpretation"
    basic_eval_interpretation
 ;;
 
 let eval_interpretation status data= 
- let status = basic_eval_interpretation data status in
- let dump = inject_interpretation data::status#dump in
-  status#set_dump dump
+ let status = basic_eval_interpretation ~alias_only:false data status in
+  NCicLibrary.dump_obj status (inject_interpretation data)
 ;;
 
 let basic_eval_alias (mode,diff) status =
@@ -112,7 +117,7 @@ let basic_eval_alias (mode,diff) status =
 
 let inject_alias =
  let basic_eval_alias (mode,diff) ~refresh_uri_in_universe ~refresh_uri_in_term
-   ~refresh_uri_in_reference =
+   ~refresh_uri_in_reference ~alias_only =
    basic_eval_alias (mode,diff)
  in
   GrafiteTypes.Serializer.register#run "alias" basic_eval_alias
@@ -120,8 +125,7 @@ let inject_alias =
 
 let eval_alias status data= 
  let status = basic_eval_alias data status in
- let dump = inject_alias data::status#dump in
-  status#set_dump dump
+  NCicLibrary.dump_obj status (inject_alias data)
 ;;
 
 let basic_eval_input_notation (l1,l2) status =
@@ -134,14 +138,18 @@ let basic_eval_input_notation (l1,l2) status =
 let inject_input_notation =
  let basic_eval_input_notation (l1,l2)
   ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
+  ~alias_only status
  =
-   let l1 =
-    CicNotationParser.refresh_uri_in_checked_l1_pattern
-     ~refresh_uri_in_term ~refresh_uri_in_reference l1 in
-   let l2 = NotationUtil.refresh_uri_in_term
-     ~refresh_uri_in_term ~refresh_uri_in_reference l2
-   in
-    basic_eval_input_notation (l1,l2)
+   if not alias_only then
+    let l1 =
+     CicNotationParser.refresh_uri_in_checked_l1_pattern
+      ~refresh_uri_in_term ~refresh_uri_in_reference l1 in
+    let l2 = NotationUtil.refresh_uri_in_term
+      ~refresh_uri_in_term ~refresh_uri_in_reference l2
+    in
+     basic_eval_input_notation (l1,l2) status
+   else
+    status
  in
   GrafiteTypes.Serializer.register#run "input_notation"
    basic_eval_input_notation
@@ -149,8 +157,7 @@ let inject_input_notation =
 
 let eval_input_notation status data= 
  let status = basic_eval_input_notation data status in
- let dump = inject_input_notation data::status#dump in
-  status#set_dump dump
+  NCicLibrary.dump_obj status (inject_input_notation data)
 ;;
 
 let basic_eval_output_notation (l1,l2) status =
@@ -160,14 +167,18 @@ let basic_eval_output_notation (l1,l2) status =
 let inject_output_notation =
  let basic_eval_output_notation (l1,l2)
   ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
+  ~alias_only status
  =
-  let l1 =
-   CicNotationParser.refresh_uri_in_checked_l1_pattern
-    ~refresh_uri_in_term ~refresh_uri_in_reference l1 in
-  let l2 = NotationUtil.refresh_uri_in_term
-    ~refresh_uri_in_term ~refresh_uri_in_reference l2
-  in
-   basic_eval_output_notation (l1,l2)
+  if not alias_only then
+   let l1 =
+    CicNotationParser.refresh_uri_in_checked_l1_pattern
+     ~refresh_uri_in_term ~refresh_uri_in_reference l1 in
+   let l2 = NotationUtil.refresh_uri_in_term
+     ~refresh_uri_in_term ~refresh_uri_in_reference l2
+   in
+    basic_eval_output_notation (l1,l2) status
+  else
+   status
  in
   GrafiteTypes.Serializer.register#run "output_notation"
    basic_eval_output_notation
@@ -175,18 +186,20 @@ let inject_output_notation =
 
 let eval_output_notation status data= 
  let status = basic_eval_output_notation data status in
- let dump = inject_output_notation data::status#dump in
-  status#set_dump dump
+  NCicLibrary.dump_obj status (inject_output_notation data)
 ;;
 
 let record_index_obj = 
  let aux l ~refresh_uri_in_universe 
-   ~refresh_uri_in_term ~refresh_uri_in_reference
+   ~refresh_uri_in_term ~refresh_uri_in_reference ~alias_only status
  =
+  if not alias_only then
     basic_index_obj
       (List.map 
         (fun ks,v -> List.map refresh_uri_in_term ks, refresh_uri_in_term v) 
-      l)
+      l) status
+  else
+   status
  in
   GrafiteTypes.Serializer.register#run "index_obj" aux
 ;;
@@ -253,8 +266,7 @@ let index_obj_for_auto status (uri, height, _, _, kind) =
  (*prerr_endline (string_of_int height);*)
   let data = compute_keys status uri height kind in
   let status = basic_index_obj data status in
-  let dump = record_index_obj data :: status#dump in   
-  status#set_dump dump
+   NCicLibrary.dump_obj status (record_index_obj data)
 ;; 
 
 let index_eq uri status =
@@ -266,7 +278,9 @@ let index_eq uri status =
 let record_index_eq =
  let basic_index_eq uri
    ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference 
-   = index_eq (NCicLibrary.refresh_uri uri) 
+   ~alias_only status
+   = if not alias_only then index_eq (NCicLibrary.refresh_uri uri) status else
+     status
  in
   GrafiteTypes.Serializer.register#run "index_eq" basic_index_eq
 ;;
@@ -277,8 +291,7 @@ let index_eq_for_auto status uri =
      if newstatus#eq_cache == status#eq_cache then status 
      else
        ((*prerr_endline ("recording " ^ (NUri.string_of_uri uri));*)
-       let dump = record_index_eq uri :: newstatus#dump 
-       in newstatus#set_dump dump)
+        NCicLibrary.dump_obj newstatus (record_index_eq uri))
  else 
    ((*prerr_endline "Not a fact";*)
    status)
@@ -290,20 +303,22 @@ let basic_eval_add_constraint (u1,u2) status =
 
 let inject_constraint =
  let basic_eval_add_constraint (u1,u2) 
-       ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
+     ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
+     ~alias_only status
  =
-  let u1 = refresh_uri_in_universe u1 in 
-  let u2 = refresh_uri_in_universe u2 in 
-  basic_eval_add_constraint (u1,u2)
+  if not alias_only then
+   let u1 = refresh_uri_in_universe u1 in 
+   let u2 = refresh_uri_in_universe u2 in 
+    basic_eval_add_constraint (u1,u2) status
+  else
+   status
  in
   GrafiteTypes.Serializer.register#run "constraints" basic_eval_add_constraint 
 ;;
 
 let eval_add_constraint status u1 u2 = 
  let status = basic_eval_add_constraint (u1,u2) status in
- let dump = inject_constraint (u1,u2)::status#dump in
- let status = status#set_dump dump in
-  status
+  NCicLibrary.dump_obj status (inject_constraint (u1,u2))
 ;;
 
 let eval_ng_tac tac =
@@ -458,14 +473,10 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
   | GrafiteAst.Include (loc, mode, fname) ->
           let _root, baseuri, _fullpath, _rrelpath = 
        Librarian.baseuri_of_script ~include_paths fname in
-     let status,obj =
-       GrafiteTypes.Serializer.require ~baseuri:(NUri.uri_of_string baseuri)
-        status in
-     let status = status#set_dump (obj::status#dump) in
-     let status = status#set_dependencies (fname::status#dependencies) in
-     (*assert false;*) (*  MATITA 1.0mode must be passed to GrafiteTypes.Serializer.require
-     somehow *)
-       status
+     let baseuri = NUri.uri_of_string baseuri in
+     (* MATITA 1.0: keep WithoutPreferences? *)
+     let alias_only = (mode = GrafiteAst.OnlyPreferences) in
+      GrafiteTypes.Serializer.require ~alias_only ~baseuri ~fname status
   | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n
   | GrafiteAst.NCoercion (loc, name, t, ty, source, target) ->
      let status, composites =