librarySync - we do not generate the object attributes when we publish the xml

[helm.git] / matita / matitaMathView.ml

diff --git a/matita/matitaMathView.ml b/matita/matitaMathView.ml
index 5ae8baab6ea2f6ee0943bdf723d275be0d3e8c4c..5c0bc953440814feedad53cfc395253fe35b49fc 100644 (file)
--- a/matita/matitaMathView.ml
+++ b/matita/matitaMathView.ml
@@ -303,9 +303,11 @@ object (self)
         "\n" ^
         GrafiteAstPp.pp_executable ~term_pp:(fun s -> s)
           ~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false)
-          (GrafiteAst.Tactical (loc,
-            GrafiteAst.Tactic (loc, GrafiteAst.Reduce (loc, kind, pat)),
-            Some (GrafiteAst.Semicolon loc))) in
+          ~map_unicode_to_tex:(Helm_registry.get_bool
+            "matita.paste_unicode_as_tex")
+          (GrafiteAst.Tactic (loc,
+            Some (GrafiteAst.Reduce (loc, kind, pat)),
+            GrafiteAst.Semicolon loc)) in
       (MatitaScript.current ())#advance ~statement () in
     connect_menu_item copy gui#copy;
     connect_menu_item normalize (reduction_action `Normalize);
@@ -434,6 +436,8 @@ object (self)
           let tactic_text_pattern =  self#tactic_text_pattern_of_node node in
           GrafiteAstPp.pp_tactic_pattern
             ~term_pp:(fun s -> s) ~lazy_term_pp:(fun _ -> assert false)
+            ~map_unicode_to_tex:(Helm_registry.get_bool
+              "matita.paste_unicode_as_tex")
             tactic_text_pattern
       | `Term -> self#tactic_text_of_node node
     else string_of_dom_node node
@@ -452,7 +456,9 @@ object (self)
     let markup = CicNotationPres.render ids_to_uris pped_ast in
     BoxPp.render_to_string text_width markup
     *)
-    ApplyTransformation.txt_of_cic_sequent_conclusion 
+    let map_unicode_to_tex =
+      Helm_registry.get_bool "matita.paste_unicode_as_tex" in
+    ApplyTransformation.txt_of_cic_sequent_conclusion ~map_unicode_to_tex
       text_width metasenv cic_sequent
 
   method private pattern_of term context unsh_sequent =
@@ -648,7 +654,9 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
       _metasenv <- []; 
       self#script#setGoal None
 
-    method load_sequents { proof = (_,metasenv,_,_) as proof; stack = stack } =
+    method load_sequents 
+      { proof = (_,metasenv,_subst,_,_, _) as proof; stack = stack } 
+    =
       _metasenv <- metasenv;
       pages <- 0;
       let win goal_switch =
@@ -844,12 +852,15 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
   let load_easter_egg = lazy (
     win#browserImage#set_file (MatitaMisc.image_path "meegg.png"))
   in
-  let load_coerchgraph () = 
+  let load_coerchgraph tred () = 
       let str = CoercGraph.generate_dot_file () in
       let filename, oc = Filename.open_temp_file "matita" ".dot" in
       output_string oc str;
       close_out oc;
-      gviz#load_graph_from_file filename;
+      if tred then
+        gviz#load_graph_from_file ~gviz_cmd:"tred|dot" filename
+      else
+        gviz#load_graph_from_file filename;
       HExtlib.safe_remove filename
   in
   object (self)
@@ -1024,13 +1035,14 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     method private _load ?(force=false) entry =
       handle_error (fun () ->
        if entry <> current_entry || entry = `About `Current_proof || entry =
-         `About `Coercions || force then
+         `About `Coercions || entry = `About `CoercionsFull || force then
         begin
           (match entry with
           | `About `Current_proof -> self#home ()
           | `About `Blank -> self#blank ()
           | `About `Us -> self#egg ()
-          | `About `Coercions -> self#coerchgraph ()
+          | `About `CoercionsFull -> self#coerchgraph false ()
+          | `About `Coercions -> self#coerchgraph true ()
           | `Check term -> self#_loadCheck term
           | `Cic (term, metasenv) -> self#_loadTermCic term metasenv
           | `Development d -> self#_showDevelDeps d
@@ -1079,20 +1091,20 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       self#redraw_gviz ~center_on:uri ();
       self#_showGviz
 
-    method private coerchgraph () =
-      load_coerchgraph ();
+    method private coerchgraph tred () =
+      load_coerchgraph tred ();
       self#_showGviz
 
     method private home () =
       self#_showMath;
       match self#script#grafite_status.proof_status with
-      | Proof  (uri, metasenv, bo, ty) ->
+      | Proof  (uri, metasenv, _subst, bo, ty, attrs) ->
           let name = UriManager.name_of_uri (HExtlib.unopt uri) in
-          let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in
+          let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], attrs) in
           self#_loadObj obj
-      | Incomplete_proof { proof = (uri, metasenv, bo, ty) } ->
+      | Incomplete_proof { proof = (uri, metasenv, _subst, bo, ty, attrs) } ->
           let name = UriManager.name_of_uri (HExtlib.unopt uri) in
-          let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in
+          let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], attrs) in
           self#_loadObj obj
       | _ -> self#blank ()
 
@@ -1104,7 +1116,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       self#_loadObj obj
       
     method private _loadDir dir = 
-      let content = Http_getter.ls dir in
+      let content = Http_getter.ls ~local:false dir in
       let l =
         List.fast_sort
           Pervasives.compare