now baseuri is needed in each file (and its redefinition is forbidden)

added exception prettyprinter

diff --git a/helm/matita/.depend b/helm/matita/.depend
index c20c1a38f4a8fc832a77c9efd5ed00c74ab0f8ed..afd46f5004c5e191411e89e48c7ae458dc9690a1 100644 (file)
--- 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 43a62c6f5110d85a2ee4972a4133f58ddf715911..57893de42a9f16ff6280f9df743b2d2604fd1a46 100644 (file)
--- 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 95de73528cf8ba1b273002e395026d11c2935d59..222ca491b9745b80eed476b5274b62f3941d2e08 100644 (file)
--- 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 b0624241a8f140c11732a911cc2e960e8d508eb0..9aa4644cbce66b55428a3f83eea32e28e93c3b88 100644 (file)
--- 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 b21c3b340e4ea0ce383993228179dd1ee151f393..c9b387178bc8cd1c780de9940d481013a1d035a0 100644 (file)
--- 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 4d0eace3ae6f7d6cf6ae1ff8b66e67b3cd05ee82..f913639f945e2f0c2919dfd2e77355d195f0144d 100644 (file)
--- 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 580f022f59baa8d0337718c9281ebcaf1331775e..9ed52f568dfd5dfe48444d45ea1a9566677063fd 100644 (file)
--- 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 954bc13966ff9a871eb71861b62ec1284776f81d..1baa34910c3a1356d5c08b0b3133a9e28a1e7f30 100644 (file)
--- 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 757d34769584e28945569dcefb79ea384956cfb1..09b80cd4ee15234d16ace68adb7fd471a6bd8a70 100644 (file)
--- 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 80256c0f4b3858e90b425d09fbcecf61d88d5e55..c6b525b2b087a236f75b71ee22f0a1597b0cf4ab 100755 (executable)
--- 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 (file)
index 0000000..3715a26
--- /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 337ef50edc1fc2a63bb1600e0ca6f0f32dc005f8..507147cef8b1802a925746acdec4b097a5bf07ca 100644 (file)
--- 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 0f642d89108e2d6d374bd1386ced1cd5a5d96c78..3e3ec9d5e985d933efb4747ea512d30968c9ab9d 100644 (file)
--- 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 27e51e69c1a6a58de495f5af6b0386195b850e2a..11396b8bdc8160327373a3c5f55037092028b575 100644 (file)
--- 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 5056f9e6ecb9f7fd75f0fe778a4111c3a7e4f7ca..d86602c5748fe9e63a25a4056934945d9b417aba 100644 (file)
--- 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 e0e302eb904b7deda398019fd85249ff609cd60b..1a6e2cac18b5c95c394d2b99d1ec1dcb1fab8ddb 100644 (file)
--- 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 70e9f414169ebae2346a6472f12055bf7bddef32..9791adecf8d4133275b19c4214374280e022daf3 100644 (file)
--- 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 e61e123d791d687bbc0323ea5f16fc0aa6f6c25a..5f173344454084a0f2fd296b9732d4ba2f16729c 100644 (file)
--- 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 24b63593cc92e9595c257d59df2758ee94c631e6..b47c5aebb3722514f536f268fad7c17b9516585b 100644 (file)
--- 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 036cc393b45214e60a96442f8bd1a4477b01017d..e36e684c2bba815d70f38d4c204e3310170b555b 100644 (file)
--- 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 1e43ce145ebaa0b181f3e9dab78297279761b239..d5df929bbfb14f791f982875f29eb51296ca1fdb 100644 (file)
--- 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 798ab27865ab91e06445e2c237b0448cc8f5ae30..b8a6d9be778ed3801e13908677e62e746a4edecd 100644 (file)
--- 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 61dec1d7e34671c1ca7a1d890b10f789ab43bec0..96463f599ea8a0968b77f437e45242602c0f7b7e 100644 (file)
--- 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 da93e1e5290d13cce17f574f6764043ef4ddd78a..67da01e89c1cab029a85b18392fed4fdcfdb30cd 100644 (file)
--- 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 8b0f1a6a0196ab225cf00b546f12e52d019aaff7..d77f91fcd0974043b22bb1a55fe3a178f6016d53 100644 (file)
--- 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 (file)
index 6c36464..0000000
--- 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 c3f3c36b8e1e877a575e8cc8124ad1c7497560a2..d622703b42bbb6bc2d246620878447563dd2b6e5 100644 (file)
--- 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 cb2cece18730d3828813b2bfe09c1f0fdace3697..08ca196829ec903829ee103ab3ec1bbb0380ac39 100644 (file)
--- 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 83b749ae03483c5871e5dd5123f177cd0093b2f7..e25472d3ca0fea11866a194a9364c7ca18524e52 100644 (file)
--- 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