X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaMathView.ml;h=8d66ff56d1f80cd2d872c606c25486abfeb78c6b;hb=2231f2820190c8743854004a9efd902d3bb5baa4;hp=c32c00f203c12c4fa99dad0730cdd3b79335bae0;hpb=05078521aaff6f41f55114e5332663b1e9706824;p=helm.git

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index c32c00f20..8d66ff56d 100644
--- a/helm/software/matita/matitaMathView.ml
+++ b/helm/software/matita/matitaMathView.ml
@@ -303,9 +303,9 @@ 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
+          (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);
@@ -452,7 +452,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_opt Helm_registry.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 +650,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 =
@@ -1090,11 +1094,11 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     method private home () =
       self#_showMath;
       match self#script#grafite_status.proof_status with
-      | Proof  (uri, metasenv, bo, ty, attrs) ->
+      | 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, [], attrs) in
           self#_loadObj obj
-      | Incomplete_proof { proof = (uri, metasenv, bo, ty, attrs) } ->
+      | 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, [], attrs) in
           self#_loadObj obj