From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 20 Jul 2005 12:49:37 +0000 (+0000)
Subject: fixed typo in 'leq interpretation uri which enable nice rendering of
X-Git-Tag: V_0_7_2~152
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ec5f1771cf795ce6186c5f0376ae248ed098d65a;p=helm.git

fixed typo in 'leq interpretation uri which enable nice rendering of
coq's le predicate
---

diff --git a/helm/matita/core_notation.ma b/helm/matita/core_notation.ma
index 88cd759b8..486e921b5 100644
--- a/helm/matita/core_notation.ma
+++ b/helm/matita/core_notation.ma
@@ -93,7 +93,7 @@ interpretation "binary integer unary minus" 'uminus x = (cic:/Coq/ZArith/BinInt/
 
 (* relational operators *)
 
-interpretation "natural 'less or equal to'" 'leq x y = (cic:/Coq/Init/Peano/le.ind x y).
+interpretation "natural 'less or equal to'" 'leq x y = (cic:/Coq/Init/Peano/le.ind#xpointer(1/1) x y).
 interpretation "real 'less or equal to'" 'leq x y = (cic:/Coq/Reals/Rdefinitions/Rle.con x y).
 interpretation "natural 'greater or equal to'" 'geq x y = (cic:/Coq/Init/Peano/ge.con x y).
 interpretation "real 'greater or equal to'" 'geq x y = (cic:/Coq/Reals/Rdefinitions/Rge.con x y).
diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 1bfd5e51e..0a3f72d4d 100644
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -181,9 +181,6 @@ let _ =
 let _ =
   at_exit (fun () -> print_endline "\nThanks for using Matita!\n");
   Sys.catch_break true;
-  (try
-     gui#loadScript Sys.argv.(1);
-   with Invalid_argument _ -> ());
   if Filename.basename Sys.argv.(0) = "cicbrowser" then begin (* cicbrowser *)
     Helm_registry.set "matita.mode" "cicbrowser";
     let browser = MatitaMathView.cicBrowser () in
@@ -195,6 +192,9 @@ let _ =
     browser#load entry
   end else begin  (* matita *)
     Helm_registry.set "matita.mode" "matita";
+    (try
+       gui#loadScript Sys.argv.(1);
+     with Invalid_argument _ -> ());
     gui#main#mainWin#show ();
   end;
   try
diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index f9171068f..cd3571ff4 100644
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -167,10 +167,9 @@ class sequentViewer obj =
       ApplyTransformation.mml_of_cic_sequent metasenv sequent
     in
     current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_hypotheses);
-(*
-    debug_print "load_sequent: dumping MathML to ./prova";
-    ignore (DomMisc.domImpl#saveDocumentToFile ~name:"./prova" ~doc:mathml ());
-*)
+    let name = "sequent_viewer.xml" in
+    prerr_endline ("load_sequent: dumping MathML to ./" ^ name);
+    ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ());
     self#load_root ~root:mathml#get_documentElement
  end
 
@@ -556,6 +555,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
           XmlDiff.update_dom ~from:current_mathml mathml;
           mathView#thaw
       |  _ ->
+          let name = "cic_browser.xml" in
+          prerr_endline ("cic_browser: dumping MathML to ./" ^ name);
+          ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ());
           mathView#load_root ~root:mathml#get_documentElement;
           current_mathml <- Some mathml);