From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 20 Sep 2005 09:01:56 +0000 (+0000)
Subject: matitadep now parses notation.
X-Git-Tag: LAST_BEFORE_NEW~88
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=65de996c8b18f6c7f7a8aeaccb83b984d62d4ce5;p=helm.git

matitadep now parses notation.
---

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index dd89c7ea4..13d946afc 100644
--- a/helm/matita/matita.txt
+++ b/helm/matita/matita.txt
@@ -89,9 +89,6 @@ TODO
   - riattaccare hbugs (brrr...) -> Zack
 
   GUI LOGICA
-  - tutte gli script che parsano (e.g. matitaclean, matitadep) debbono
-    processare la notazione per evitare errori di parsing (visibili ora
-    che e' stata committata la contrib list)!
   - la funzione alias_diff e' lentissima (anche se CSC l'ha accellerata di
     un fattore 3x) e puo' essere evitata: chi vuole aggiungere alias (la
     disambiguazione, il comando "alias" e l'add_obj) deve indicare
@@ -120,6 +117,9 @@ TODO
   DEMONI E ALTRO
 
 DONE
+- tutte gli script che parsano (e.g. matitaclean, matitadep) debbono
+  processare la notazione per evitare errori di parsing (visibili ora
+  che e' stata committata la contrib list)! -> Gares
 - E' possibile fare "Build" senza selezionare nulla, ottenendo un
   assert false -> Gares
 - disambiguazione: attualmente io (CSC) ho committato la versione di
diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml
index 308dd95d2..a795f5f4b 100644
--- a/helm/matita/matitacLib.ml
+++ b/helm/matita/matitacLib.ml
@@ -205,13 +205,13 @@ let main ~mode =
     let elapsed = Unix.time () -. time in
     let tm = Unix.gmtime elapsed in
     let sec = 
-      if tm.Unix.tm_sec > 0 then  (string_of_int tm.Unix.tm_sec ^ "''") else "" 
+      if tm.Unix.tm_sec > 0 then (string_of_int tm.Unix.tm_sec ^ "''") else "" 
     in
     let min = 
-      if tm.Unix.tm_min > 0 then  (string_of_int tm.Unix.tm_min ^ "' ") else "" 
+      if tm.Unix.tm_min > 0 then (string_of_int tm.Unix.tm_min ^ "' ") else "" 
     in
     let hou = 
-      if tm.Unix.tm_hour > 0 then (string_of_int tm.Unix.tm_hour ^ "h ") else "" 
+      if tm.Unix.tm_hour > 0 then (string_of_int tm.Unix.tm_hour ^ "h ") else ""
     in
     let proof_status,moo_content_rev = 
       match !status with
diff --git a/helm/matita/matitadep.ml b/helm/matita/matitadep.ml
index 0676aa93e..4e260dcf6 100644
--- a/helm/matita/matitadep.ml
+++ b/helm/matita/matitadep.ml
@@ -35,7 +35,7 @@ let usage =
   Printf.sprintf "MatitaDep v%s\nUsage: matitadep [options] file...\nOptions:"
     BuildTimeConf.version
 
-module TA = GrafiteAst 
+module GA = GrafiteAst 
 module U = UriManager
 
 let deps = Hashtbl.create (Array.length Sys.argv)
@@ -75,6 +75,26 @@ let find path =
     raise exc
 ;;
 
+(* note, this function works cause moo files are transitively closed *)
+let process_notation_of_file file =
+    let ic = open_in file in
+    let istream = Stream.of_channel ic in
+    let notation_ids = ref [] in
+    try
+      while true do
+        match GrafiteParser.parse_statement istream with
+        | GA.Executable (_, GA.Command (_, notation)) ->
+          let stm, ids = CicNotation.process_notation notation in
+          notation_ids := ids @ !notation_ids
+        | _ -> ()
+      done; []
+    with
+    | End_of_file -> close_in ic; !notation_ids
+    | CicNotationParser.Parse_error _ as exn ->
+        prerr_endline ("Unable to parse: " ^ file);
+        prerr_endline (MatitaExcPp.to_string exn);
+        raise exn
+
 let main () =
   Helm_registry.load_from BuildTimeConf.matita_conf;
   CicNotation.load_notation BuildTimeConf.core_notation_script;
@@ -84,20 +104,34 @@ let main () =
    (fun file -> 
     let ic = open_in file in
     let istream = Stream.of_channel ic in
+    let notation_ids = ref [] in
     (try
       while true do
         try 
-          match GrafiteParser.parse_statement istream with
-          | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", uri))) ->
+          let stm = GrafiteParser.parse_statement istream in
+          (match stm with 
+          | GA.Executable (_, GA.Command (_, notation)) ->
+            let stm, ids = CicNotation.process_notation notation in
+            notation_ids := ids @ !notation_ids
+          | _ -> ());
+          match stm with
+          | GA.Executable (_, GA.Command (_, GA.Set (_, "baseuri", uri))) ->
               let uri = MatitaMisc.strip_trailing_slash uri in
               baseuris := uri :: !baseuris
-          | TA.Executable (_, TA.Command 
-              (_, TA.Alias (_, TA.Ident_alias(_, uri)))) -> 
+          | GA.Executable (_, GA.Command 
+              (_, GA.Alias (_, GA.Ident_alias(_, uri)))) -> 
                 Hashtbl.add aliases file uri
-          | TA.Executable (_, TA.Command (_, TA.Include (_, path))) ->
-             if path <> "coq.ma" then
+          | GA.Executable (_, GA.Command (_, GA.Include (_, path))) ->
+              (* maybe to process coq.ma is useles since it contains only
+               * interpretations... no idea if notations will be added later *)
+              let moo_file = 
+                MatitaMisc.obj_file_of_script (
+                  if path <> "coq.ma" then find path else path)
+              in
+              let ids = process_notation_of_file moo_file in
+              notation_ids := ids @ !notation_ids;
               (try
-                Hashtbl.add deps file (MatitaMisc.obj_file_of_script (find path))
+                Hashtbl.add deps file moo_file
                with
                 Sys_error _ ->
                  MatitaLog.error
@@ -118,7 +152,9 @@ let main () =
         match dep with 
         | None -> ()
         | Some u -> Hashtbl.add deps file (MatitaMisc.obj_file_of_baseuri u))
-      aliases
+      aliases;
+    (* remove notation ids *)
+    List.iter CicNotation.remove_notation !notation_ids;
    ) !files;
   List.iter
    (fun file ->