From 13fab17e3d3dee05df676985c065ae54a5766870 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 25 Jul 2005 10:16:06 +0000 Subject: [PATCH] merged transformations on top of notation code --- helm/matita/.cvsignore | 1 + helm/matita/buildTimeConf.ml.in | 1 + helm/matita/configure.ac | 1 + helm/matita/core_notation.ma | 30 ++++++++-------------- helm/matita/dictionary-matita.xml | 15 +++++++++++ helm/matita/gtkmathview.matita.conf.xml.in | 15 +++++++++++ helm/matita/matita.ml | 2 ++ 7 files changed, 46 insertions(+), 19 deletions(-) create mode 100644 helm/matita/dictionary-matita.xml create mode 100644 helm/matita/gtkmathview.matita.conf.xml.in diff --git a/helm/matita/.cvsignore b/helm/matita/.cvsignore index bf527ad6c..1498f4892 100644 --- a/helm/matita/.cvsignore +++ b/helm/matita/.cvsignore @@ -38,3 +38,4 @@ matitamake.opt matita.conf.xml *.moo matita.conf.xml.sample +gtkmathview.matita.conf.xml diff --git a/helm/matita/buildTimeConf.ml.in b/helm/matita/buildTimeConf.ml.in index b38eb2ce4..5ceabc66f 100644 --- a/helm/matita/buildTimeConf.ml.in +++ b/helm/matita/buildTimeConf.ml.in @@ -42,6 +42,7 @@ let lang_file = runtime_base_dir ^ "/matita.lang" let script_template = runtime_base_dir ^ "/matita.ma.templ" let core_notation_script = runtime_base_dir ^ "/core_notation.ma" let matita_conf = runtime_base_dir ^ "/matita.conf.xml" +let gtkmathview_conf = runtime_base_dir ^ "/gtkmathview.matita.conf.xml" let matitamake_makefile_template = runtime_base_dir ^ "/template_makefile.in" diff --git a/helm/matita/configure.ac b/helm/matita/configure.ac index 678cc2342..ce2d82432 100644 --- a/helm/matita/configure.ac +++ b/helm/matita/configure.ac @@ -112,4 +112,5 @@ AC_OUTPUT([ matita.conf.xml.sample buildTimeConf.ml Makefile + gtkmathview.matita.conf.xml ]) diff --git a/helm/matita/core_notation.ma b/helm/matita/core_notation.ma index 486e921b5..680ebb7b5 100644 --- a/helm/matita/core_notation.ma +++ b/helm/matita/core_notation.ma @@ -2,6 +2,10 @@ notation "hvbox(a break \to b)" right associative with precedence 20 for @{ \forall $_:$a.$b }. +notation < "hvbox(a break \to b)" + right associative with precedence 20 +for @{ \Pi $_:$a.$b }. + notation "hvbox(a break = b)" non associative with precedence 45 for @{ 'eq $a $b }. @@ -91,6 +95,13 @@ interpretation "real unary minus" 'uminus x = (cic:/Coq/Reals/Rdefinitions/Ropp. interpretation "binary integer negative sign" 'uminus x = (cic:/Coq/ZArith/BinInt/Z.ind#xpointer(1/1/3) x). interpretation "binary integer unary minus" 'uminus x = (cic:/Coq/ZArith/BinInt/Zopp.con x). +(* logical operators *) + +interpretation "logical and" 'and x y = (cic:/Coq/Init/Logic/and.ind#xpointer(1/1) x y). +interpretation "logical or" 'or x y = (cic:/Coq/Init/Logic/or.ind#xpointer(1/1) x y). +interpretation "logical not" 'not x = (cic:/Coq/Init/Logic/not.con x). +interpretation "exists" 'exists x y = (cic:/Coq/Init/Logic/ex.ind#xpointer(1/1) x y). + (* relational operators *) interpretation "natural 'less or equal to'" 'leq x y = (cic:/Coq/Init/Peano/le.ind#xpointer(1/1) x y). @@ -105,22 +116,3 @@ interpretation "real 'greater than'" 'gt x y = (cic:/Coq/Reals/Rdefinitions/Rgt. interpretation "leibnitz's equality" 'eq x y = (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1) _ x y). interpretation "not equal to (leibnitz)" 'neq x y = (cic:/Coq/Init/Logic/not.con (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1) _ x y)). -(* logical operators *) - -interpretation "logical and" 'and x y = (cic:/Coq/Init/Logic/and.ind#xpointer(1/1) x y). -interpretation "logical or" 'or x y = (cic:/Coq/Init/Logic/or.ind#xpointer(1/1) x y). -interpretation "logical not" 'not x = (cic:/Coq/Init/Logic/not.con x). -interpretation "exists" 'exists x y = (cic:/Coq/Init/Logic/ex.ind#xpointer(1/1) x y). - -(* - add_symbol_choice "cast" - ("type cast", - (fun env _ args -> - let t1, t2 = - match args with - | [t1; t2] -> t1, t2 - | _ -> raise Invalid_choice - in - Cic.Cast (t1, t2))); -*) - diff --git a/helm/matita/dictionary-matita.xml b/helm/matita/dictionary-matita.xml new file mode 100644 index 000000000..4f883e7af --- /dev/null +++ b/helm/matita/dictionary-matita.xml @@ -0,0 +1,15 @@ + + + + + + + + + + + + + + + diff --git a/helm/matita/gtkmathview.matita.conf.xml.in b/helm/matita/gtkmathview.matita.conf.xml.in new file mode 100644 index 000000000..0a33ae6d0 --- /dev/null +++ b/helm/matita/gtkmathview.matita.conf.xml.in @@ -0,0 +1,15 @@ + + +
+ @RT_BASE_DIR@/dictionary-matita.xml +
+
+
+
+
+ normal +
+
+
+
+ diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index d4f9c3fac..aae334abd 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -44,6 +44,8 @@ let _ = MatitaDb.create_owner_environment (); MatitamakeLib.initialize (); GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file; (* loads gtk rc *) + prerr_endline BuildTimeConf.gtkmathview_conf; + GMathView.add_configuration_path BuildTimeConf.gtkmathview_conf; ignore (GMain.Main.init ()); CicEnvironment.set_trust (* environment trust *) (let trust = Helm_registry.get_bool "matita.environment_trust" in -- 2.39.2