From: Enrico Tassi 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 ->