From 2a4ee6db10333354003f6e3cd342298a82799ad4 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Nov 2007 13:12:25 +0000 Subject: [PATCH] snapshot for camlp5 v5 --- DEVEL/gdome_xslt/debian/changelog | 6 - DEVEL/gdome_xslt/debian/control | 1 - DEVEL/lablgtkmathview/debian/changelog | 24 --- DEVEL/lablgtkmathview/debian/control | 11 +- Makefile | 1 + .../syntax_extensions/pa_unicode_macro.ml | 5 +- configure.ac | 6 +- daemons/on-line/xslt/getParam.xsl | 2 +- daemons/on-line/xslt/ls2theory.xsl | 2 +- daemons/on-line/xslt/makeGraphLinks.xsl | 2 +- daemons/on-line/xslt/metadataControl.xsl | 2 +- daemons/on-line/xslt/substKey.xsl | 4 +- daemons/rdfly/Makefile | 2 +- daemons/rdfly/rdfly.conf.xml.sample | 21 +-- daemons/rdfly/rdfly.ml | 171 ++++++++++-------- matita/matita.conf.xml.in | 2 + matita/matitaInit.ml | 1 + matita/matitaMathView.ml | 7 +- matita/matitaScript.ml | 3 +- 19 files changed, 133 insertions(+), 140 deletions(-) diff --git a/DEVEL/gdome_xslt/debian/changelog b/DEVEL/gdome_xslt/debian/changelog index 3af2b012f..de0da2d25 100644 --- a/DEVEL/gdome_xslt/debian/changelog +++ b/DEVEL/gdome_xslt/debian/changelog @@ -1,9 +1,3 @@ -gdome2-xslt (0.0.8-3) unstable; urgency=low - - * add Homepage debian/control field - - -- Stefano Zacchiroli Sat, 22 Sep 2007 08:57:56 +0200 - gdome2-xslt (0.0.8-2) unstable; urgency=low * debian/rules diff --git a/DEVEL/gdome_xslt/debian/control b/DEVEL/gdome_xslt/debian/control index 6c821f3ce..62ed73d29 100644 --- a/DEVEL/gdome_xslt/debian/control +++ b/DEVEL/gdome_xslt/debian/control @@ -4,7 +4,6 @@ Priority: optional Maintainer: Stefano Zacchiroli Build-Depends: debhelper (>= 5.0.0), ocaml-nox (>= 3.10.0), ocaml-findlib (>= 1.1), libgdome2-ocaml-dev (>= 0.2.5-3), libgdome2-dev (>= 0.8.1), libxslt1-dev, libgdome2-cpp-smart-dev (>= 0.2.4), pkg-config, cdbs Standards-Version: 3.7.2 -Homepage: http://helm.cs.unibo.it/software/gdome_xslt/ XS-Vcs-Svn: svn://mowgli.cs.unibo.it/trunk/helm/software/DEVEL/gdome_xslt XS-Vcs-Browser: http://helm.cs.unibo.it/websvn/listing.php?path=/trunk/helm/software/DEVEL/gdome_xslt/ diff --git a/DEVEL/lablgtkmathview/debian/changelog b/DEVEL/lablgtkmathview/debian/changelog index 2a85588f4..91003c55a 100644 --- a/DEVEL/lablgtkmathview/debian/changelog +++ b/DEVEL/lablgtkmathview/debian/changelog @@ -1,27 +1,3 @@ -lablgtkmathview (0.7.8-4) UNRELEASED; urgency=low - - * NOT RELEASED YET - - -- Stefano Zacchiroli Fri, 23 Nov 2007 14:25:16 +0100 - -lablgtkmathview (0.7.8-3) unstable; urgency=low - - * bump deps on lablgtk2 to match lates upstream - * debian/control - - fix VCS field names (now supported natively by dpkg) - - add Homepage field - - -- Stefano Zacchiroli Fri, 23 Nov 2007 13:59:38 +0100 - -lablgtkmathview (0.7.8-2) unstable; urgency=low - - * debian/liblablgtkmathview-ocaml-dev.install.in - - more flexible pattern to install ocaml object files, so that missing - *.cmxa files on non-native arch do not trigger failure with latest - debhelper - - -- Stefano Zacchiroli Sat, 15 Sep 2007 17:40:45 +0200 - lablgtkmathview (0.7.8-1) unstable; urgency=low * add ocamldoc comments to .mli interface files diff --git a/DEVEL/lablgtkmathview/debian/control b/DEVEL/lablgtkmathview/debian/control index 3ca8997d4..a17a54ee3 100644 --- a/DEVEL/lablgtkmathview/debian/control +++ b/DEVEL/lablgtkmathview/debian/control @@ -2,16 +2,15 @@ Source: lablgtkmathview Section: devel Priority: optional Maintainer: Stefano Zacchiroli -Build-Depends: debhelper (>> 5.0.0), cdbs, ocaml-nox (>= 3.10.0), ocaml-findlib (>= 1.1), liblablgtk2-ocaml-dev (>= 2.10.0), libgdome2-ocaml-dev (>= 0.2.5-3), libgtkmathview-dev (>= 0.7.5), pkg-config +Build-Depends: debhelper (>> 5.0.0), cdbs, ocaml-nox (>= 3.10.0), ocaml-findlib (>= 1.1), liblablgtk2-ocaml-dev (>= 2.6.0-13), libgdome2-ocaml-dev (>= 0.2.5-3), libgtkmathview-dev (>= 0.7.5), pkg-config Standards-Version: 3.7.2 -Vcs-Svn: svn://mowgli.cs.unibo.it/trunk/helm/software/DEVEL/lablgtkmathview -Vcs-Browser: http://helm.cs.unibo.it/websvn/listing.php?path=/trunk/helm/software/DEVEL/lablgtkmathview/ -Homepage: http://helm.cs.unibo.it/mml-widget/ +XS-Vcs-Svn: svn://mowgli.cs.unibo.it/trunk/helm/software/DEVEL/lablgtkmathview +XS-Vcs-Browser: http://helm.cs.unibo.it/websvn/listing.php?path=/trunk/helm/software/DEVEL/lablgtkmathview/ Package: liblablgtkmathview-ocaml Architecture: any Section: libs -Depends: ocaml-base-nox-${F:OCamlABI}, liblablgtk2-ocaml (>= 2.10.0), libgdome2-ocaml (>= 0.2.3-5), libgtkmathview0c2a (>= 0.7.5), ${shlibs:Depends}, ${misc:Depends} +Depends: ocaml-base-nox-${F:OCamlABI}, liblablgtk2-ocaml (>= 2.6.0-2), libgdome2-ocaml (>= 0.2.3-5), libgtkmathview0c2a (>= 0.7.5), ${shlibs:Depends}, ${misc:Depends} Description: OCaml bindings for libgtkmathview, a GTK widget to render MathML This is the Ocaml binding for the GtkMathView widget, that is currently available in the libgtkmathview0 package. @@ -21,7 +20,7 @@ Description: OCaml bindings for libgtkmathview, a GTK widget to render MathML Package: liblablgtkmathview-ocaml-dev Architecture: any Section: libdevel -Depends: ocaml-nox-${F:OCamlABI}, liblablgtk2-ocaml-dev (>= 2.10.0), liblablgtkmathview-ocaml (= ${binary:Version}), ocaml-findlib, libgdome2-ocaml-dev (>= 0.2.5-3), libgtkmathview-dev (>= 0.7.5), ${misc:Depends} +Depends: ocaml-nox-${F:OCamlABI}, liblablgtk2-ocaml-dev (>= 2.6.0-13), liblablgtkmathview-ocaml (= ${binary:Version}), ocaml-findlib, libgdome2-ocaml-dev (>= 0.2.5-3), libgtkmathview-dev (>= 0.7.5), ${misc:Depends} Description: OCaml bindings for libgtkmathview, a GTK widget to render MathML These are the Ocaml bindings for the GtkMathView widget, that is currently available in the libgtkmathview0 package. diff --git a/Makefile b/Makefile index 2f19a7523..44b87c579 100644 --- a/Makefile +++ b/Makefile @@ -56,6 +56,7 @@ CLEAN_ON_DIST = \ components/license \ matita/TPTP/ \ matita/dama/ \ + matita/dama_didactic/ \ matita/contribs/ \ matita/library_auto/ \ $(NULL) diff --git a/components/syntax_extensions/pa_unicode_macro.ml b/components/syntax_extensions/pa_unicode_macro.ml index 436766862..a0051edfc 100644 --- a/components/syntax_extensions/pa_unicode_macro.ml +++ b/components/syntax_extensions/pa_unicode_macro.ml @@ -51,9 +51,12 @@ EXTEND String.sub q (pos + 1) (String.length q - pos - 1)) in debug_print (lazy (Printf.sprintf "QUOTATION = %s; ARG = %s" quotation arg)); - if quotation = "unicode" then + if quotation = "unicode" then + AStok (loc, x, Some (ATexpr (loc, expand_unicode_macro arg))) +(* let text = TXtok (loc, x, expand_unicode_macro arg) in {used = []; text = text; styp = STlid (loc, "string")} +*) else assert false ] diff --git a/configure.ac b/configure.ac index a20df9d4c..f985336ca 100644 --- a/configure.ac +++ b/configure.ac @@ -5,7 +5,7 @@ AC_INIT(matita/matitaTypes.ml) DEBUG_DEFAULT="true" DEFAULT_DBHOST="mysql://mowgli.cs.unibo.it" RT_BASE_DIR_DEFAULT="`pwd`/matita" -MATITA_VERSION="0.4.97" +MATITA_VERSION="0.4.98" DISTRIBUTED="no" # "yes" for distributed tarballs # End of distribution settings @@ -62,8 +62,8 @@ expat \ gdome2 \ http \ lablgtk2 \ +lablgtksourceview.gtksourceview \ lablgtkmathview \ -lablgtksourceview \ mysql \ netstring \ ulex08 \ @@ -91,7 +91,7 @@ FINDLIB_REQUIRES="\ $FINDLIB_CREQUIRES \ lablgtk2.glade \ lablgtkmathview \ -lablgtksourceview \ +lablgtksourceview.gtksourceview \ helm-xmldiff \ " for r in $FINDLIB_LIBSREQUIRES $FINDLIB_REQUIRES diff --git a/daemons/on-line/xslt/getParam.xsl b/daemons/on-line/xslt/getParam.xsl index 8caeee9ea..14d09f07b 100644 --- a/daemons/on-line/xslt/getParam.xsl +++ b/daemons/on-line/xslt/getParam.xsl @@ -7,7 +7,7 @@ diff --git a/daemons/on-line/xslt/ls2theory.xsl b/daemons/on-line/xslt/ls2theory.xsl index 91942331b..3e9e4abec 100644 --- a/daemons/on-line/xslt/ls2theory.xsl +++ b/daemons/on-line/xslt/ls2theory.xsl @@ -6,7 +6,7 @@ xmlns="http://www.w3.org/1999/xhtml" > - + diff --git a/daemons/on-line/xslt/makeGraphLinks.xsl b/daemons/on-line/xslt/makeGraphLinks.xsl index 13f440216..62c68d227 100644 --- a/daemons/on-line/xslt/makeGraphLinks.xsl +++ b/daemons/on-line/xslt/makeGraphLinks.xsl @@ -37,7 +37,7 @@ - + diff --git a/daemons/on-line/xslt/metadataControl.xsl b/daemons/on-line/xslt/metadataControl.xsl index d4fb97d95..b548037a5 100644 --- a/daemons/on-line/xslt/metadataControl.xsl +++ b/daemons/on-line/xslt/metadataControl.xsl @@ -12,7 +12,7 @@ diff --git a/daemons/on-line/xslt/substKey.xsl b/daemons/on-line/xslt/substKey.xsl index 4172956b6..76b29991b 100644 --- a/daemons/on-line/xslt/substKey.xsl +++ b/daemons/on-line/xslt/substKey.xsl @@ -8,13 +8,13 @@ - /tmp/ - - web - -
- mysql://mowgli.cs.unibo.it public helm none library - mysql://mowgli.cs.unibo.it mowgli helm none legacy - file:///tmp/ dust.db helm none user -
+
+ localhost + helm + mowgli + 3306 +
58086
diff --git a/daemons/rdfly/rdfly.ml b/daemons/rdfly/rdfly.ml index 9b2a08d2a..8dbb6b051 100644 --- a/daemons/rdfly/rdfly.ml +++ b/daemons/rdfly/rdfly.ml @@ -1,15 +1,19 @@ -module Registry = Helm_registry -module SQL = HSql -module DB = LibraryDb - -let exec_and_iter dbd query f = - let db_types = [SQL.Library; SQL.Legacy] in - let map db_type = - let res = SQL.exec db_type dbd query in - SQL.iter res ~f - in - List.iter map db_types +module M = Mysql + + (* First of all we load the configuration *) +let _ = + let configuration_file = "/projects/helm/etc/rdfly.conf.xml" in + Helm_registry.load_from configuration_file +;; + +let open_db ?host ?database ?port ?password ?user = + try + M.quick_connect ?host ?database ?port ?password ?user + with + M.Error e as exc -> + prerr_endline e ; + raise exc let extract_position s = let sharp_pos = String.rindex s '#' + 1 in @@ -33,101 +37,120 @@ let msg_output_dc_header msg obj = msg_output_string msg "\n\n" ; msg_output_string msg ("\n") ; msg_output_string msg " " +;; let msg_output_dc_trailer msg = msg_output_string msg " \n" +;; let value_of_optional_value = function None -> assert false | Some v -> v +;; -let forward_metadata dbd obj = +let forward_metadata db obj = + let res = M.exec db ("SELECT * FROM refObj WHERE source = '" ^ obj ^ "';") in let msg = mk_new_msg () in - let query = "SELECT * FROM refObj WHERE source = '" ^ obj ^ "';" in - let map cols = + msg_output_header msg obj ; + M.iter res + ~f:(function cols -> let position = extract_position (value_of_optional_value (cols.(2))) in let occurrence = value_of_optional_value (cols.(1)) in msg_output_string msg " \n \n" ; msg_output_string msg (" " ^ position ^ "\n") ; msg_output_string msg (" " ^ occurrence ^ "\n") ; msg_output_string msg " \n \n" - in - msg_output_header msg obj ; - exec_and_iter dbd query map ; + ) ; msg_output_trailer msg ; msg_serialize msg +;; -let backward_metadata dbd obj = +let backward_metadata db obj = + let res = M.exec db ("SELECT * FROM refObj WHERE h_occurrence = '" ^ obj ^ "';") in let msg = mk_new_msg () in - let query = "SELECT * FROM refObj WHERE h_occurrence = '" ^ obj ^ "';" in - let map cols = + msg_output_header msg obj ; + M.iter res + ~f:(function cols -> let position = extract_position (value_of_optional_value (cols.(2))) in let occurrence = value_of_optional_value (cols.(0)) in msg_output_string msg " \n \n" ; msg_output_string msg (" " ^ position ^ "\n") ; msg_output_string msg (" " ^ occurrence ^ "\n") ; msg_output_string msg " \n \n" - in - msg_output_header msg obj ; - exec_and_iter dbd query map ; + ) ; msg_output_trailer msg ; msg_serialize msg +;; -let dc_metadata dbd obj = - let tables = - [ "dc:creator","dccreator" ; - "dc:date","dcdate" ; - "dc:description","dcdescription" ; - "dc:format","dcformat" ; - "dc:identifier","dcidentifier" ; - "dc:language","dclanguage" ; - "dc:publisher","dcpublisher" ; - "dcq:RelationType","dcqRelationType" ; - "dc:relation","dcrelation" ; - "dc:rights","dcrights" ; - "dc:source","dcsource" ; - "dc:subject","dcsubject" ; - "dc:title","dctitle" ; - "hth:ResourceFormat","hthResourceFormat" ; - "hth:contact","hthcontact" ; - "hth:firstVersion","hthfirstVersion" ; - "hth:institution","hthinstitution" ; - "hth:modified","hthmodified" - ] - in - let msg = mk_new_msg () in - let table_map (propertyname, tablename) = - let query = "SELECT * FROM " ^ tablename ^ " WHERE uri = '" ^ obj ^ "';" in - let map cols = - let value = value_of_optional_value (cols.(0)) in - msg_output_string msg - (" <" ^ propertyname ^ ">" ^ value ^ "\n") - in - exec_and_iter dbd query map - in - msg_output_dc_header msg obj ; - List.iter table_map tables ; +let dc_metadata db obj = + let tables = + [ "dc:creator","dccreator" ; + "dc:date","dcdate" ; + "dc:description","dcdescription" ; + "dc:format","dcformat" ; + "dc:identifier","dcidentifier" ; + "dc:language","dclanguage" ; + "dc:publisher","dcpublisher" ; + "dcq:RelationType","dcqRelationType" ; + "dc:relation","dcrelation" ; + "dc:rights","dcrights" ; + "dc:source","dcsource" ; + "dc:subject","dcsubject" ; + "dc:title","dctitle" ; + "hth:ResourceFormat","hthResourceFormat" ; + "hth:contact","hthcontact" ; + "hth:firstVersion","hthfirstVersion" ; + "hth:institution","hthinstitution" ; + "hth:modified","hthmodified" + ] + in + let msg = mk_new_msg () in + msg_output_dc_header msg obj ; + List.iter + (fun (propertyname,tablename) -> + let res = + M.exec db + ("SELECT * FROM " ^ tablename ^ " WHERE uri = '" ^ obj ^ "';") in + M.iter res + ~f:(function cols -> + let value = value_of_optional_value (cols.(0)) in + msg_output_string msg + (" <" ^ propertyname ^ ">" ^ value ^ "\n") ; + ) ; + ) tables ; msg_output_dc_trailer msg ; msg_serialize msg +;; let debug_print s = prerr_endline ("[RDFly] " ^ s) let mk_return_fun contype msg outchan = Http_daemon.respond ~body:msg ~headers:["Content-Type", contype] outchan - + let return_html = mk_return_fun "text/html" let return_xml = mk_return_fun "text/xml" let return_400 body ch = Http_daemon.respond_error ~code:(`Code 400) ~body ch let return_html_error s = return_html ("" ^ s ^ "") -(* First of all we load the configuration *) -let configuration_file = "/projects/helm/etc/rdfly.conf.xml" -let _ = Registry.load_from configuration_file -let db_spec = DB.parse_dbd_conf () -let daemonport = Helm_registry.get_int "rdfly.port" +let get_option key = + try + Some (Helm_registry.get key) + with Helm_registry.Key_not_found _ -> None + +let get_int_option key = + try + Some (Helm_registry.get_int key) + with Helm_registry.Key_not_found _ -> None + +let host = get_option "rdfly.mysql_connection.host";; +let database = get_option "rdfly.mysql_connection.database";; +let port = get_int_option "rdfly.mysql_connection.port";; +let password = get_option "rdfly.mysql_connection.password";; +let user = get_option "rdfly.mysql_connection.user";; +let daemonport = Helm_registry.get_int "rdfly.port";; let callback (req: Http_types.request) ch = try @@ -137,17 +160,17 @@ let callback (req: Http_types.request) ch = | "/help" -> return_html_error "yeah right..." ch | "/get" -> - let obj = req#param "object" in - let kind = req#param "kind" in - let dbd = SQL.quick_connect db_spec in + let obj = req#param "object" + and kind = req#param "kind" in + let db = open_db ?host ?database ?port ?password ?user () in begin match kind with - "forward" -> return_xml (forward_metadata dbd obj) ch - | "backward" -> return_xml (backward_metadata dbd obj) ch - | "dc" -> return_xml (dc_metadata dbd obj) ch + "forward" -> return_xml (forward_metadata db obj) ch + | "backward" -> return_xml (backward_metadata db obj) ch + | "dc" -> return_xml (dc_metadata db obj) ch | s -> return_html_error ("unsupported kind: " ^ s) ch end ; - SQL.disconnect dbd + M.disconnect db | invalid_request -> Http_daemon.respond_error ~code:(`Status (`Client_error `Bad_request)) ch) @@ -155,17 +178,17 @@ let callback (req: Http_types.request) ch = | Http_types.Param_not_found attr_name -> return_400 (Printf.sprintf "Parameter '%s' is missing" attr_name) ch | exc -> - prerr_endline (Printexc.to_string exc); return_html_error ("Uncaught exception: " ^ (Printexc.to_string exc)) ch let main () = - Sys.catch_break true; + Sys.catch_break true; try let d_spec = Http_daemon.daemon_spec ~timeout:(Some 600) ~port:daemonport ~callback ~auto_close:true () in Http_daemon.main d_spec with Sys.Break -> () -;; - +in + main () + diff --git a/matita/matita.conf.xml.in b/matita/matita.conf.xml.in index e88a4fc5a..3d2630199 100644 --- a/matita/matita.conf.xml.in +++ b/matita/matita.conf.xml.in @@ -22,6 +22,8 @@ $(user.name) + +