]> matita.cs.unibo.it Git - helm.git/commitdiff
snapshot for camlp5 v5
authorEnrico Tassi <enrico.tassi@inria.fr>
Sun, 25 Nov 2007 13:12:25 +0000 (13:12 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Sun, 25 Nov 2007 13:12:25 +0000 (13:12 +0000)
19 files changed:
DEVEL/gdome_xslt/debian/changelog
DEVEL/gdome_xslt/debian/control
DEVEL/lablgtkmathview/debian/changelog
DEVEL/lablgtkmathview/debian/control
Makefile
components/syntax_extensions/pa_unicode_macro.ml
configure.ac
daemons/on-line/xslt/getParam.xsl
daemons/on-line/xslt/ls2theory.xsl
daemons/on-line/xslt/makeGraphLinks.xsl
daemons/on-line/xslt/metadataControl.xsl
daemons/on-line/xslt/substKey.xsl
daemons/rdfly/Makefile
daemons/rdfly/rdfly.conf.xml.sample
daemons/rdfly/rdfly.ml
matita/matita.conf.xml.in
matita/matitaInit.ml
matita/matitaMathView.ml
matita/matitaScript.ml

index 3af2b012f6289ed8e61b6bf20b5023b520ac66d1..de0da2d251896243233d320e27aa38399b83a28a 100644 (file)
@@ -1,9 +1,3 @@
-gdome2-xslt (0.0.8-3) unstable; urgency=low
-
-  * add Homepage debian/control field
-
- -- Stefano Zacchiroli <zack@debian.org>  Sat, 22 Sep 2007 08:57:56 +0200
-
 gdome2-xslt (0.0.8-2) unstable; urgency=low
 
   * debian/rules
index 6c821f3cef36a1b4e762c404e09b124a28471b1c..62ed73d29303ddd277a7006f34d7e639e70825ef 100644 (file)
@@ -4,7 +4,6 @@ Priority: optional
 Maintainer: Stefano Zacchiroli <zack@debian.org>
 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/
 
index 2a85588f4d0ca9036ec6449c892614aca14e6fdf..91003c55a3a284e6ad6d31557346e7417184e2c7 100644 (file)
@@ -1,27 +1,3 @@
-lablgtkmathview (0.7.8-4) UNRELEASED; urgency=low
-
-  * NOT RELEASED YET
-
- -- Stefano Zacchiroli <zack@debian.org>  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 <zack@debian.org>  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 <zack@debian.org>  Sat, 15 Sep 2007 17:40:45 +0200
-
 lablgtkmathview (0.7.8-1) unstable; urgency=low
 
   * add ocamldoc comments to .mli interface files
index 3ca8997d4d97988ace323447fb4e29d387b6812f..a17a54ee391ad5a7a3206be275535d6e77ae0127 100644 (file)
@@ -2,16 +2,15 @@ Source: lablgtkmathview
 Section: devel
 Priority: optional
 Maintainer: Stefano Zacchiroli <zack@debian.org>
-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.
index 2f19a75239a319b733934251d99ec792170a3831..44b87c579a6b3216bbd663d1436cd4cd465bd15d 100644 (file)
--- 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)
index 436766862b714ba78af312270b60b669ef0c35f3..a0051edfc9290491239f7407305ffaa2edd1e3fa 100644 (file)
@@ -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
       ]
index a20df9d4c53e35930fb7a5be5d1a38fbd1558cad..f985336ca5a45f8f84fd16ddf2fd01ed2dbf9f63 100644 (file)
@@ -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
index 8caeee9eae40db213c5b62ee4241ed73af57cf66..14d09f07b7e2efa9d04e3006d12802b1b5d096df 100644 (file)
@@ -7,7 +7,7 @@
 
 <xsl:output 
        method="xml"
-       encoding="UTF-8" 
+       encoding="utf8" 
        media-type="text/html"
        doctype-public="-//W3C//DTD XHTML 1.0 Transitional//EN"
        doctype-system="http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd" />
index 91942331bb1c2827aa58c16dea6ed15a0b778977..3e9e4abec3d4f48100b4bd15f4664abea74c352f 100644 (file)
@@ -6,7 +6,7 @@
   xmlns="http://www.w3.org/1999/xhtml"
 >
 
-  <xsl:output method="html" encoding="UTF-8"/>
+  <xsl:output method="html" encoding="utf8"/>
 
   <xsl:param name="CICURI" select="''" />
   <xsl:param name="interfaceURL" select="''" />
index 13f44021651d6a517e6a2b2b1cceda73835ff3cb..62c68d227160b319180ed032743c16e66c13dd40 100644 (file)
@@ -37,7 +37,7 @@
 <xsl:param name="uri_set_size" select="''"/>
 <!--CSC: end of cut & paste also in metadataLib.xsl -->
 
-<xsl:output method="html" encoding="UTF-8"/>
+<xsl:output method="html" encoding="utf8"/>
 
 <xsl:template match="/|*">
   <xsl:copy>
index d4fb97d950f9189ea9d7cb15560e801a35ab1c11..b548037a5ba8667041cca0b6b98da6e08e29d158 100644 (file)
@@ -12,7 +12,7 @@
 
 <xsl:output 
        method="xml"
-       encoding="UTF-8" 
+       encoding="utf8" 
        media-type="text/html"
        doctype-public="-//W3C//DTD XHTML 1.0 Transitional//EN"
        doctype-system="http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd" />
index 4172956b6415d6ddbcd7c7f56b5b37483ed2ff2d..76b29991b29671ed8ee8e7e63adb924389e8d623 100644 (file)
@@ -8,13 +8,13 @@
 
 <xsl:output
        method="html"
-       encoding="UTF-8"
+       encoding="utf8"
        doctype-public="-//W3C//DTD XHTML 1.0 Transitional//EN"
        media-type="text/html" />
 <!--
 <xsl:output
         method="xml"
-        encoding="UTF-8"
+        encoding="utf8"
         media-type="text/xml"
         doctype-public="-//W3C//DTD XHTML 1.0 Transitional//EN"
         doctype-system="DTD/xhtml1-transitional.dtd" />
index a762f5273bbf3a2a3c2a97c8011068ebbb33b39d..26e296409b4765f4a31459680df41ff2ee4c5da1 100644 (file)
@@ -1,5 +1,5 @@
 BIN_DIR = /usr/local/bin
-REQUIRES = http helm-registry helm-hmysql helm-library
+REQUIRES = mysql http helm-registry
 PREDICATES = 
 OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o
 ifeq ($(origin OCAMLPATH), undefined)
index 9e3efb3f2ae9f4d6e2eebc8df9de7ea0a4323e1a..5d479dacfd34b4e85634a31c2504c1e395ef87f4 100644 (file)
@@ -1,19 +1,12 @@
+<?xml version="1.0" encoding="utf-8"?>
 <helm_registry>
-  <section name="user">
-    <!-- User home directory. Here a ".matita" directory will be created
-    and used to store the part of the library developed by the user. -->
-    <key name="home">/tmp/</key>
-    <!-- User name. It is used down in this configuration file.  If left
-    unspecified, name of the user executing matita will be used (as per
-    getent) -->
-    <key name="name">web</key>
-  </section>
-  <section name="db">
-    <key name="metadata">mysql://mowgli.cs.unibo.it public helm none library</key>
-    <key name="metadata">mysql://mowgli.cs.unibo.it mowgli helm none legacy</key>
-    <key name="metadata">file:///tmp/ dust.db helm none user</key>
-  </section>
   <section name="rdfly">
+    <section name="mysql_connection">
+      <key name="host">localhost</key>
+      <key name="user">helm</key>
+      <key name="database">mowgli</key>
+      <key name="port">3306</key>
+    </section>
     <key name="port">58086</key>
   </section>
 </helm_registry>
index 9b2a08d2a742bcd91f42bca94f0251012e6c4512..8dbb6b051c484a48101d68f590a3adeb18c87d75 100644 (file)
@@ -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 "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n\n" ;
   msg_output_string msg ("<rdf:RDF xml:lang=\"en\"\n         xmlns:rdf=\"http://www.w3.org/1999/02/22-rdf-syntax-ns#\"\n         xmlns:rdfs=\"http://www.w3.org/2000/01/rdf-schema#\"\n         xmlns:dc=\"http://purl.org/metadata/dublin_core#\"\n         xmlns:dcq=\"http://purl.org/metadata/dublin_core_qualifiers#\"\n         xmlns:h=\"http:/www.cs.unibo.it/helm/schemas/schema-h.rdf#\"\n         xmlns:hth=\"http://www.cs.unibo.it/helm/schemas/schema-hth.rdf#\">\n") ;
   msg_output_string msg "  <h:DirectoryOfObjects>"
+;;
 
 let msg_output_dc_trailer msg =
   msg_output_string msg "  </h:DirectoryOfObjects>\n</rdf:RDF>"
+;;
 
 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 "    <h:refObj>\n      <h:Occurrence>\n" ;
      msg_output_string msg ("        <h:position>" ^ position ^ "</h:position>\n") ;
      msg_output_string msg ("        <h:occurrence>" ^ occurrence ^ "</h:occurrence>\n") ;
      msg_output_string msg "      </h:Occurrence>\n    </h:refObj>\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 "    <h:backPointer>\n      <h:Occurrence>\n" ;
      msg_output_string msg ("        <h:position>" ^ position ^ "</h:position>\n") ;
      msg_output_string msg ("        <h:occurrence>" ^ occurrence ^ "</h:occurrence>\n") ;
      msg_output_string msg "      </h:Occurrence>\n    </h:backPointer>\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 ^ "</" ^ propertyname ^ ">\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 ^ "</" ^ propertyname ^ ">\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 ("<html><body>" ^ s ^ "</body></html>")
 
-(* 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 ()
+
index e88a4fc5a8104987bbc89528848fb8f0c7994201..3d26301990c6ba29628c645c44bc19f4b5d1e231 100644 (file)
@@ -22,6 +22,8 @@
     <key name="owner">$(user.name)</key>
     <!-- Initial GUI font size. -->
     <!-- <key name="font_size">10</key> -->
+    <!--  Perform heavy checks when run interactively (like duplicate check) -->
+    <!-- <key name="do_heavy_checks">false</key> -->
   </section>
   <section name="db">
     <!-- 
index 8ae9b00a37fb0e325058428be5ade6bb957abc66..076cae5e9c88902db4dad7768df7851600e1f366 100644 (file)
@@ -52,6 +52,7 @@ let registry_defaults = [
   "matita.bench",                "false";
   "matita.paste_unicode_as_tex", "false";
   "matita.noinnertypes",         "false";
+  "matita.do_heavy_checks",      "true";
     (** verbosity level: 1 is the default, 0 is intuitively "quiet", > 1 is
      * intuitively verbose *)
 ]
index b8dd3f1bdcb5bb2d5e0f01428aaf08306ac06fec..23f57820df80601337c8ba86ff5b958a0f428383 100644 (file)
@@ -620,11 +620,11 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
 
     method load_logo =
      notebook#set_show_tabs false;
-     notebook#append_page logo
+     ignore(notebook#append_page logo)
 
     method load_logo_with_qed =
      notebook#set_show_tabs false;
-     notebook#append_page logo_with_qed
+     ignore(notebook#append_page logo_with_qed)
 
     method reset =
       cicMathView#remove_selections;
@@ -698,7 +698,8 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
       let add_tab markup goal_switch =
         let goal = Stack.goal_of_switch goal_switch in
         if not (List.mem goal !added_goals) then begin
-          notebook#append_page ~tab_label:(tab_label markup) (win goal_switch);
+          ignore(notebook#append_page 
+            ~tab_label:(tab_label markup) (win goal_switch));
           page2goal <- (!page, goal_switch) :: page2goal;
           goal2page <- (goal_switch, !page) :: goal2page;
           incr page;
index c29e15533ef1c6a71a10c06b04a46cec6f95481a..8ec2a4948bcc7c6bc19608d03f59a1089aa0468f 100644 (file)
@@ -85,7 +85,8 @@ let eval_with_engine guistuff lexicon_status grafite_status user_goal
   let text = skipped_txt ^ nonskipped_txt in
   let prefix_len = MatitaGtkMisc.utf8_string_length skipped_txt in
   let enriched_history_fragment =
-   MatitaEngine.eval_ast ~do_heavy_checks:true
+   MatitaEngine.eval_ast ~do_heavy_checks:(Helm_registry.get_bool
+     "matita.do_heavy_checks")
     lexicon_status grafite_status (text,prefix_len,st)
   in
   let enriched_history_fragment = List.rev enriched_history_fragment in