From d9394782ed9580f3565eb9b4682d8348aae6349e Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 29 Jun 2005 13:52:42 +0000
Subject: [PATCH] now baseuri is needed in each file (and its redefinition is
 forbidden) added exception prettyprinter

---
 helm/matita/.depend                      | 8 ++++++--
 helm/matita/Makefile.in                  | 2 ++
 helm/matita/matitaEngine.ml              | 4 +++-
 helm/matita/matitaGtkMisc.ml             | 7 -------
 helm/matita/matitaGui.ml                 | 4 +---
 helm/matita/matitaMathView.ml            | 2 +-
 helm/matita/matitaTypes.ml               | 5 ++++-
 helm/matita/matitacLib.ml                | 2 +-
 helm/matita/tests/apply.ma               | 1 +
 helm/matita/tests/auto.ma                | 2 ++
 helm/matita/tests/baseuri.ma             | 2 ++
 helm/matita/tests/coercions.ma           | 2 ++
 helm/matita/tests/comments.ma            | 2 ++
 helm/matita/tests/fguidi.ma              | 2 ++
 helm/matita/tests/fix_betareduction.ma   | 2 ++
 helm/matita/tests/interactive/drop.ma    | 2 ++
 helm/matita/tests/interactive/grafite.ma | 4 +++-
 helm/matita/tests/inversion.ma           | 4 +++-
 helm/matita/tests/letrec.ma              | 2 ++
 helm/matita/tests/match.ma               | 2 ++
 helm/matita/tests/match_inference.ma     | 2 ++
 helm/matita/tests/mysql_escaping.ma      | 2 ++
 helm/matita/tests/record.ma              | 4 +++-
 helm/matita/tests/rewrite.ma             | 4 +++-
 helm/matita/tests/simpl.ma               | 4 +++-
 helm/matita/tests/test1.ma               | 6 ------
 helm/matita/tests/test2.ma               | 4 +++-
 helm/matita/tests/test3.ma               | 2 ++
 helm/matita/tests/test4.ma               | 2 ++
 29 files changed, 63 insertions(+), 28 deletions(-)
 create mode 100644 helm/matita/tests/baseuri.ma
 delete mode 100644 helm/matita/tests/test1.ma

diff --git a/helm/matita/.depend b/helm/matita/.depend
index c20c1a38f..afd46f500 100644
--- a/helm/matita/.depend
+++ b/helm/matita/.depend
@@ -12,14 +12,18 @@ matitaEngine.cmo: matitaTypes.cmo matitaSync.cmi matitaMisc.cmi matitaLog.cmi \
     matitaDisambiguator.cmi matitaDb.cmi matitaEngine.cmi 
 matitaEngine.cmx: matitaTypes.cmx matitaSync.cmx matitaMisc.cmx matitaLog.cmx \
     matitaDisambiguator.cmx matitaDb.cmx matitaEngine.cmi 
+matitaExcPp.cmo: matitaTypes.cmo matitaExcPp.cmi 
+matitaExcPp.cmx: matitaTypes.cmx matitaExcPp.cmi 
 matitaGeneratedGui.cmo: matitaGeneratedGui.cmi 
 matitaGeneratedGui.cmx: matitaGeneratedGui.cmi 
 matitaGtkMisc.cmo: matitaTypes.cmo matitaGeneratedGui.cmi matitaGtkMisc.cmi 
 matitaGtkMisc.cmx: matitaTypes.cmx matitaGeneratedGui.cmx matitaGtkMisc.cmi 
 matitaGui.cmo: matitaTypes.cmo matitaScript.cmi matitaMisc.cmi matitaLog.cmi \
-    matitaGtkMisc.cmi matitaGeneratedGui.cmi buildTimeConf.cmo matitaGui.cmi 
+    matitaGtkMisc.cmi matitaGeneratedGui.cmi matitaExcPp.cmi \
+    buildTimeConf.cmo matitaGui.cmi 
 matitaGui.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx matitaLog.cmx \
-    matitaGtkMisc.cmx matitaGeneratedGui.cmx buildTimeConf.cmx matitaGui.cmi 
+    matitaGtkMisc.cmx matitaGeneratedGui.cmx matitaExcPp.cmx \
+    buildTimeConf.cmx matitaGui.cmi 
 matitaLog.cmo: matitaLog.cmi 
 matitaLog.cmx: matitaLog.cmi 
 matitaMathView.cmo: matitaTypes.cmo matitaScript.cmi matitaMisc.cmi \
diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in
index 43a62c6f5..57893de42 100644
--- a/helm/matita/Makefile.in
+++ b/helm/matita/Makefile.in
@@ -21,6 +21,7 @@ CMOS =				\
 	buildTimeConf.cmo	\
 	matitaLog.cmo		\
 	matitaTypes.cmo		\
+	matitaExcPp.cmo 	\
 	matitaMisc.cmo		\
 	matitaDb.cmo		\
 	matitaSync.cmo		\
@@ -36,6 +37,7 @@ CCMOS =				\
 	buildTimeConf.cmo	\
 	matitaLog.cmo		\
 	matitaTypes.cmo		\
+	matitaExcPp.cmo 	\
 	matitaMisc.cmo		\
 	matitaDb.cmo		\
 	matitaSync.cmo		\
diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 95de73528..222ca491b 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -585,16 +585,18 @@ let eval_string status str =
   eval_from_stream status (Stream.of_string str) (fun _ _ -> ())
 
 let default_options () =
+(*
   let options =
     StringMap.add "baseuri"
       (String
         (Helm_registry.get "matita.baseuri" ^ Helm_registry.get "matita.owner"))
       no_options
   in
+*)
   let options =
     StringMap.add "basedir"
       (String (Helm_registry.get "matita.basedir" ))
-      options
+      no_options
   in
   options
 
diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml
index b0624241a..9aa4644cb 100644
--- a/helm/matita/matitaGtkMisc.ml
+++ b/helm/matita/matitaGtkMisc.ml
@@ -29,13 +29,6 @@ open Printf
 open MatitaTypes
 
 let wrap_callback f = f
-(*
-let wrap_callback f () =
-  try
-    f ()
-  with exn ->
-    MatitaLog.error (sprintf "Uncaught exception: %s" (Printexc.to_string exn))
-*)
 
 let connect_button (button: #GButton.button) callback =
   ignore (button#connect#clicked (wrap_callback callback))
diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index b21c3b340..c9b387178 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -186,9 +186,7 @@ class gui () =
         (* log *)
       MatitaLog.set_log_callback self#console#log_callback;
       GtkSignal.user_handler :=
-        (fun exn ->
-           MatitaLog.error
-             (sprintf "Uncaught exception: %s" (Printexc.to_string exn)));
+        (fun exn -> MatitaLog.error (MatitaExcPp.to_string exn));
         (* script *)
       let _ =
         match GSourceView.source_language_from_file BuildTimeConf.lang_file with
diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index 4d0eace3a..f913639f9 100644
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -361,7 +361,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     try
       f ()
     with exn ->
-      fail (sprintf "Uncaught exception:\n%s" (Printexc.to_string exn))
+      fail (MatitaExcPp.to_string exn)
   in
   let handle_error' f = (fun () -> handle_error (fun () -> f ())) in
   object (self)
diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index 580f022f5..9ed52f568 100644
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -126,7 +126,10 @@ let set_option status name value =
         with Failure _ ->
           command_error (sprintf "Not an integer value \"%s\"" value))
   in
-  { status with options = StringMap.add name value status.options }
+  if StringMap.mem name status.options && name = "baseuri" then
+    command_error "Redefinition of 'baseuri' is forbidden."
+  else
+    { status with options = StringMap.add name value status.options }
 
   (* subset of MatitaConsole.console methods needed by MatitaInterpreter *)
 class type console =
diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml
index 954bc1396..1baa34910 100644
--- a/helm/matita/matitacLib.ml
+++ b/helm/matita/matitacLib.ml
@@ -65,7 +65,7 @@ let run_script is eval_function  =
   | MatitaEngine.Drop  
   | CicTextualParser2.Parse_error _ as exn -> raise exn
   | exn -> 
-      MatitaLog.error (Printexc.to_string exn);
+      MatitaLog.error (MatitaExcPp.to_string exn);
       raise exn
 
 let fname () =
diff --git a/helm/matita/tests/apply.ma b/helm/matita/tests/apply.ma
index 757d34769..09b80cd4e 100644
--- a/helm/matita/tests/apply.ma
+++ b/helm/matita/tests/apply.ma
@@ -1,4 +1,5 @@
 (* test _with_ the WHD on the apply argument *)
+set "baseuri" "cic:/matita/tests/".
 
 alias id "not" = "cic:/Coq/Init/Logic/not.con".
 alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)".
diff --git a/helm/matita/tests/auto.ma b/helm/matita/tests/auto.ma
index 80256c0f4..c6b525b2b 100755
--- a/helm/matita/tests/auto.ma
+++ b/helm/matita/tests/auto.ma
@@ -1,3 +1,5 @@
+set "baseuri" "cic:/matita/tests/".
+
 alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
 alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)".
 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
diff --git a/helm/matita/tests/baseuri.ma b/helm/matita/tests/baseuri.ma
new file mode 100644
index 000000000..3715a268a
--- /dev/null
+++ b/helm/matita/tests/baseuri.ma
@@ -0,0 +1,2 @@
+set "baseuri" "cic:/matita/tests/".
+set "baseuri" "cic:/matita/tests/".
diff --git a/helm/matita/tests/coercions.ma b/helm/matita/tests/coercions.ma
index 337ef50ed..507147cef 100644
--- a/helm/matita/tests/coercions.ma
+++ b/helm/matita/tests/coercions.ma
@@ -1,3 +1,5 @@
+set "baseuri" "cic:/matita/tests/".
+
 inductive pos: Set \def
 | one : pos
 | next : pos \to pos.
diff --git a/helm/matita/tests/comments.ma b/helm/matita/tests/comments.ma
index 0f642d891..3e3ec9d5e 100644
--- a/helm/matita/tests/comments.ma
+++ b/helm/matita/tests/comments.ma
@@ -12,6 +12,8 @@
 (*                                                                          *)
 (****************************************************************************)
 
+set "baseuri" "cic:/matita/tests/".
+
 (* commento che va nell'ast, ma non viene contato
     come step perche' non e' un executable
 *)
diff --git a/helm/matita/tests/fguidi.ma b/helm/matita/tests/fguidi.ma
index 27e51e69c..11396b8bd 100644
--- a/helm/matita/tests/fguidi.ma
+++ b/helm/matita/tests/fguidi.ma
@@ -1,3 +1,5 @@
+set "baseuri" "cic:/matita/tests/".
+
 alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
 alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)".
diff --git a/helm/matita/tests/fix_betareduction.ma b/helm/matita/tests/fix_betareduction.ma
index 5056f9e6e..d86602c57 100644
--- a/helm/matita/tests/fix_betareduction.ma
+++ b/helm/matita/tests/fix_betareduction.ma
@@ -1,3 +1,5 @@
+set "baseuri" "cic:/matita/tests/".
+
 alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)".
 alias id "n" = "cic:/Suresnes/BDD/canonicite/Canonicity_BDT/n.con".
 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
diff --git a/helm/matita/tests/interactive/drop.ma b/helm/matita/tests/interactive/drop.ma
index e0e302eb9..1a6e2cac1 100644
--- a/helm/matita/tests/interactive/drop.ma
+++ b/helm/matita/tests/interactive/drop.ma
@@ -1,3 +1,5 @@
+set "baseuri" "cic:/matita/tests/".
+
 alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
 alias num (instance 0) = "natural number".
 alias symbol "eq" (instance 0) = "leibnitz's equality".
diff --git a/helm/matita/tests/interactive/grafite.ma b/helm/matita/tests/interactive/grafite.ma
index 70e9f4141..9791adecf 100644
--- a/helm/matita/tests/interactive/grafite.ma
+++ b/helm/matita/tests/interactive/grafite.ma
@@ -1,4 +1,6 @@
-%% test per temperino.lang
+%% test per matita.lang
+
+set "baseuri" "cic:/matita/tests/".
 
 %% commento
 (* commento *)
diff --git a/helm/matita/tests/inversion.ma b/helm/matita/tests/inversion.ma
index e61e123d7..5f1733444 100644
--- a/helm/matita/tests/inversion.ma
+++ b/helm/matita/tests/inversion.ma
@@ -1,3 +1,5 @@
+set "baseuri" "cic:/matita/tests/".
+
 inductive nat : Set \def
    O : nat
  | S : nat \to nat.
@@ -19,4 +21,4 @@ theorem test_inversion: \forall n. le n O \to n=O.
   intro. reflexivity.
   simplify. intros.
   discriminate H3.
-qed.
\ No newline at end of file
+qed.
diff --git a/helm/matita/tests/letrec.ma b/helm/matita/tests/letrec.ma
index 24b63593c..b47c5aebb 100644
--- a/helm/matita/tests/letrec.ma
+++ b/helm/matita/tests/letrec.ma
@@ -1,3 +1,5 @@
+set "baseuri" "cic:/matita/tests/".
+
 
 alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
 alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)".
diff --git a/helm/matita/tests/match.ma b/helm/matita/tests/match.ma
index 036cc393b..e36e684c2 100644
--- a/helm/matita/tests/match.ma
+++ b/helm/matita/tests/match.ma
@@ -12,6 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+set "baseuri" "cic:/matita/tests/".
+
 
 inductive True: Prop \def
 I : True.
diff --git a/helm/matita/tests/match_inference.ma b/helm/matita/tests/match_inference.ma
index 1e43ce145..d5df929bb 100644
--- a/helm/matita/tests/match_inference.ma
+++ b/helm/matita/tests/match_inference.ma
@@ -1,3 +1,5 @@
+set "baseuri" "cic:/matita/tests/".
+
 inductive pos: Set \def
 | one : pos
 | next : pos \to pos.
diff --git a/helm/matita/tests/mysql_escaping.ma b/helm/matita/tests/mysql_escaping.ma
index 798ab2786..b8a6d9be7 100644
--- a/helm/matita/tests/mysql_escaping.ma
+++ b/helm/matita/tests/mysql_escaping.ma
@@ -1,3 +1,5 @@
+set "baseuri" "cic:/matita/tests/".
+
 theorem a' : Prop \to Prop.intros.assumption.qed.
 
 
diff --git a/helm/matita/tests/record.ma b/helm/matita/tests/record.ma
index 61dec1d7e..96463f599 100644
--- a/helm/matita/tests/record.ma
+++ b/helm/matita/tests/record.ma
@@ -1,3 +1,5 @@
+set "baseuri" "cic:/matita/tests/".
+
 record empty : Type \def {}.
 
 inductive True : Prop \def I: True.
@@ -20,4 +22,4 @@ record paperino: Prop \def {
   paolo : Type;
   pippo : paolo \to paolo;
   piero : True
-}.
\ No newline at end of file
+}.
diff --git a/helm/matita/tests/rewrite.ma b/helm/matita/tests/rewrite.ma
index da93e1e52..67da01e89 100644
--- a/helm/matita/tests/rewrite.ma
+++ b/helm/matita/tests/rewrite.ma
@@ -1,3 +1,5 @@
+set "baseuri" "cic:/matita/tests/".
+
 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
 alias num (instance 0) = "natural number".
 alias symbol "eq" (instance 0) = "leibnitz's equality". 
@@ -18,4 +20,4 @@ rewrite right H in \vdash (? ? ? (% ?)).
 simplify.
 reflexivity.
 qed.
- 
\ No newline at end of file
+ 
diff --git a/helm/matita/tests/simpl.ma b/helm/matita/tests/simpl.ma
index 8b0f1a6a0..d77f91fcd 100644
--- a/helm/matita/tests/simpl.ma
+++ b/helm/matita/tests/simpl.ma
@@ -1,3 +1,5 @@
+set "baseuri" "cic:/matita/tests/".
+
 alias id "not" = "cic:/Coq/Init/Logic/not.con".
 alias symbol "eq" (instance 0) = "leibnitz's equality".
 theorem a : 
@@ -9,4 +11,4 @@ simplify.
 intro. apply H.
 symmetry.
 exact H1.
-qed.
\ No newline at end of file
+qed.
diff --git a/helm/matita/tests/test1.ma b/helm/matita/tests/test1.ma
deleted file mode 100644
index 6c3646409..000000000
--- a/helm/matita/tests/test1.ma
+++ /dev/null
@@ -1,6 +0,0 @@
-set "baseuri" "cic:/matita/zack/aaa/".
-inductive nat:Set \def O:nat | S:nat \to nat.
-set "baseuri" "cic:/matita/zack/bbb/".
-inductive nat:Set \def O:nat | S:nat \to nat.
-alias id "nat" = "cic:/matita/zack/bbb/nat.ind#xpointer(1/1)".
-inductive c:Set \def c1: nat \to c.
diff --git a/helm/matita/tests/test2.ma b/helm/matita/tests/test2.ma
index c3f3c36b8..d622703b4 100644
--- a/helm/matita/tests/test2.ma
+++ b/helm/matita/tests/test2.ma
@@ -1,3 +1,5 @@
+set "baseuri" "cic:/matita/tests/".
+
 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
 alias symbol "and" (instance 0) = "logical and".
 alias symbol "eq" (instance 0) = "leibnitz's equality".
@@ -6,4 +8,4 @@ intro.
 split.
 reflexivity.
 reflexivity.
-qed.
\ No newline at end of file
+qed.
diff --git a/helm/matita/tests/test3.ma b/helm/matita/tests/test3.ma
index cb2cece18..08ca19682 100644
--- a/helm/matita/tests/test3.ma
+++ b/helm/matita/tests/test3.ma
@@ -1,3 +1,5 @@
+set "baseuri" "cic:/matita/tests/".
+
 alias symbol "eq" (instance 0) = "leibnitz's equality".
 theorem a:\forall x.x=x.
 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
diff --git a/helm/matita/tests/test4.ma b/helm/matita/tests/test4.ma
index 83b749ae0..e25472d3c 100644
--- a/helm/matita/tests/test4.ma
+++ b/helm/matita/tests/test4.ma
@@ -1,3 +1,5 @@
+set "baseuri" "cic:/matita/tests/".
+
 
 (* commento che va nell'ast, ma non viene contato
     come step perche' non e' un executable
-- 
2.39.2