From: Enrico Tassi Date: Wed, 5 Jul 2006 10:40:11 +0000 (+0000) Subject: bugfix to developments: X-Git-Tag: 0.4.95@7852~1243 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=81b53ddc3ce92187e62deff483919ca2251fd246;p=helm.git bugfix to developments: - if an included .ma file is not found (not in CWD, not in include_paths) an error is issued - if an included .ma file is found but the corrsponding .lexicon is not found a development for the .ma is searched: - if found it is used to compile the .ma file - if not found the user is aked to create a devel for the file included (and not the file that he is editing, that may not be in the same devel). --- diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml index b066b8ae0..ad5423b3e 100644 --- a/components/grafite_engine/grafiteEngine.ml +++ b/components/grafite_engine/grafiteEngine.ml @@ -28,7 +28,8 @@ open Printf exception Drop -exception IncludedFileNotCompiled of string (* file name *) +(* mo file name, ma file name *) +exception IncludedFileNotCompiled of string * string exception Macro of GrafiteAst.loc * (Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) @@ -581,7 +582,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status let moopath = if Sys.file_exists moopath_r then moopath_r else if Sys.file_exists moopath_rw then moopath_rw else - raise (IncludedFileNotCompiled moopath_rw) + raise (IncludedFileNotCompiled (moopath_rw,baseuri)) in let status = eval_from_moo.efm_go status moopath in status,[] diff --git a/components/grafite_engine/grafiteEngine.mli b/components/grafite_engine/grafiteEngine.mli index b1df57281..8363971ae 100644 --- a/components/grafite_engine/grafiteEngine.mli +++ b/components/grafite_engine/grafiteEngine.mli @@ -24,7 +24,7 @@ *) exception Drop -exception IncludedFileNotCompiled of string +exception IncludedFileNotCompiled of string * string exception Macro of GrafiteAst.loc * (Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) diff --git a/components/grafite_parser/dependenciesParser.ml b/components/grafite_parser/dependenciesParser.ml index 686caa5b1..74cf0aa77 100644 --- a/components/grafite_parser/dependenciesParser.ml +++ b/components/grafite_parser/dependenciesParser.ml @@ -86,4 +86,4 @@ let baseuri_of_script ~include_paths file = let uri = Http_getter_misc.strip_trailing_slash buri in if String.length uri < 5 || String.sub uri 0 5 <> "cic:/" then HLog.error (file ^ " sets an incorrect baseuri: " ^ buri); - uri + uri,file diff --git a/components/grafite_parser/dependenciesParser.mli b/components/grafite_parser/dependenciesParser.mli index 882d45fb8..6a8d2ae21 100644 --- a/components/grafite_parser/dependenciesParser.mli +++ b/components/grafite_parser/dependenciesParser.mli @@ -36,4 +36,5 @@ val pp_dependency: dependency -> string (** @raise End_of_file *) val parse_dependencies: Ulexing.lexbuf -> dependency list -val baseuri_of_script : include_paths:string list -> string -> string +(* returns baseuri and the full path of the script *) +val baseuri_of_script : include_paths:string list -> string -> string * string diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index f99573b30..1a11ec62f 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -539,15 +539,18 @@ EXTEND fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com)) | (iloc,fname,mode) = include_command ; SYMBOL "." -> fun ~include_paths status -> - let path = DependenciesParser.baseuri_of_script ~include_paths fname in + let buri, fullpath = + DependenciesParser.baseuri_of_script ~include_paths fname + in let status = - LexiconEngine.eval_command status (LexiconAst.Include (iloc,path,mode)) + LexiconEngine.eval_command status + (LexiconAst.Include (iloc,buri,mode,fullpath)) in status, LSome (GrafiteAst.Executable (loc,GrafiteAst.Command - (loc,GrafiteAst.Include (iloc,path)))) + (loc,GrafiteAst.Include (iloc,buri)))) | scom = lexicon_command ; SYMBOL "." -> fun ~include_paths status -> let status = LexiconEngine.eval_command status scom in diff --git a/components/lexicon/lexiconAst.ml b/components/lexicon/lexiconAst.ml index 50f0061ee..9fb188d48 100644 --- a/components/lexicon/lexiconAst.ml +++ b/components/lexicon/lexiconAst.ml @@ -41,7 +41,7 @@ let magic = 5 type inclusion_mode = WithPreferences | WithoutPreferences (* aka aliases *) type command = - | Include of loc * string * inclusion_mode + | Include of loc * string * inclusion_mode * string (* _,buri,_,path *) | Alias of loc * alias_spec (** parameters, name, type, fields *) | Notation of loc * direction option * CicNotationPt.term * Gramext.g_assoc * diff --git a/components/lexicon/lexiconAstPp.ml b/components/lexicon/lexiconAstPp.ml index 23f008296..0b2c94639 100644 --- a/components/lexicon/lexiconAstPp.ml +++ b/components/lexicon/lexiconAstPp.ml @@ -77,7 +77,7 @@ let pp_notation dir_opt l1_pattern assoc prec l2_pattern = (pp_l2_pattern l2_pattern) let pp_command = function - | Include (_,path,mode) -> + | Include (_,_,mode,path) -> (* not precise, since path is absolute *) if mode = WithPreferences then "include " ^ path else diff --git a/components/lexicon/lexiconEngine.ml b/components/lexicon/lexiconEngine.ml index 34e314edc..1e1fe61c0 100644 --- a/components/lexicon/lexiconEngine.ml +++ b/components/lexicon/lexiconEngine.ml @@ -25,7 +25,8 @@ (* $Id$ *) -exception IncludedFileNotCompiled of string (* file name *) +(* lexicon file name * ma file name *) +exception IncludedFileNotCompiled of string * string exception MetadataNotFound of string (* file name *) type status = { @@ -115,7 +116,7 @@ let rec eval_command ?(mode=LexiconAst.WithPreferences) status cmd = let status = { status with notation_ids = notation_ids' @ status.notation_ids } in match cmd with - | LexiconAst.Include (loc, baseuri, mode) -> + | LexiconAst.Include (loc, baseuri, mode, fullpath) -> let lexiconpath_rw, lexiconpath_r = LibraryMisc.lexicon_file_of_baseuri ~must_exist:false ~writable:true ~baseuri, @@ -125,7 +126,7 @@ let rec eval_command ?(mode=LexiconAst.WithPreferences) status cmd = let lexiconpath = if Sys.file_exists lexiconpath_rw then lexiconpath_rw else if Sys.file_exists lexiconpath_r then lexiconpath_r else - raise (IncludedFileNotCompiled lexiconpath_rw) + raise (IncludedFileNotCompiled (lexiconpath_rw,fullpath)) in let lexicon = LexiconMarshal.load_lexicon lexiconpath in let status = List.fold_left (eval_command ~mode) status lexicon in diff --git a/components/lexicon/lexiconEngine.mli b/components/lexicon/lexiconEngine.mli index 8e8b420ba..00201c9fb 100644 --- a/components/lexicon/lexiconEngine.mli +++ b/components/lexicon/lexiconEngine.mli @@ -23,7 +23,7 @@ * http://helm.cs.unibo.it/ *) -exception IncludedFileNotCompiled of string +exception IncludedFileNotCompiled of string * string type status = { aliases: DisambiguateTypes.environment; (** disambiguation aliases *) diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml index 510e736e5..5674063e9 100644 --- a/matita/matitaScript.ml +++ b/matita/matitaScript.ml @@ -106,59 +106,71 @@ let eval_with_engine guistuff lexicon_status grafite_status user_goal res,parsed_text_length let wrap_with_developments guistuff f arg = + let compile_needed_and_go_on lexiconfile d exc = + let target = Pcre.replace ~pat:"lexicon$" ~templ:"moo" lexiconfile in + let target = Pcre.replace ~pat:"metadata$" ~templ:"moo" target in + let refresh_cb () = + while Glib.Main.pending () do ignore(Glib.Main.iteration false); done + in + if not(MatitamakeLib.build_development_in_bg ~target refresh_cb d) then + raise exc + else + f arg + in + let do_nothing () = raise (ActionCancelled "Inclusion not performed") in + let check_if_file_is_exists f = + assert(Pcre.pmatch ~pat:"ma$" f); + let pwd = Sys.getcwd () in + let f_pwd = pwd ^ "/" ^ f in + if not (HExtlib.is_regular f_pwd) then + raise (ActionCancelled ("File "^f_pwd^" does not exists!")) + else + raise + (ActionCancelled + ("Internal error: "^f_pwd^" exists but I'm unable to include it!")) + in + let handle_with_devel d lexiconfile exc = + let name = MatitamakeLib.name_for_development d in + let title = "Unable to include " ^ lexiconfile in + let message = + lexiconfile ^ " is handled by development " ^ name ^ ".\n\n" ^ + "Should I compile it and Its dependencies?" + in + (match guistuff.ask_confirmation ~title ~message with + | `YES -> compile_needed_and_go_on lexiconfile d exc + | `NO -> raise exc + | `CANCEL -> do_nothing ()) + in + let handle_without_devel mafilename exc = + let title = "Unable to include " ^ mafilename in + let message = + mafilename ^ " is not handled by a development.\n" ^ + "All dependencies are automatically solved for a development.\n\n" ^ + "Do you want to set up a development?" + in + (match guistuff.ask_confirmation ~title ~message with + | `YES -> + guistuff.develcreator ~containing:(Some (Filename.dirname mafilename)); + do_nothing () + | `NO -> raise exc + | `CANCEL -> do_nothing()) + in try f arg with - | DependenciesParser.UnableToInclude what - | LexiconEngine.IncludedFileNotCompiled what - | GrafiteEngine.IncludedFileNotCompiled what as exc -> - let compile_needed_and_go_on d = - let target = Pcre.replace ~pat:"lexicon$" ~templ:"moo" what in - let refresh_cb () = - while Glib.Main.pending () do ignore(Glib.Main.iteration false); done - in - if not(MatitamakeLib.build_development_in_bg ~target refresh_cb d) then - raise exc - else - f arg - in - let do_nothing () = raise (ActionCancelled "Inclusion not performed") in - let handle_with_devel d = - let name = MatitamakeLib.name_for_development d in - let title = "Unable to include " ^ what in - let message = - what ^ " is handled by development " ^ name ^ ".\n\n" ^ - "Should I compile it and Its dependencies?" - in - (match guistuff.ask_confirmation ~title ~message with - | `YES -> compile_needed_and_go_on d - | `NO -> raise exc - | `CANCEL -> do_nothing ()) - in - let handle_without_devel filename = - let title = "Unable to include " ^ what in - let message = - what ^ " is not handled by a development.\n" ^ - "All dependencies are automatically solved for a development.\n\n" ^ - "Do you want to set up a development?" - in - (match guistuff.ask_confirmation ~title ~message with - | `YES -> - (match filename with - | Some f -> - guistuff.develcreator ~containing:(Some (Filename.dirname f)) - | None -> guistuff.develcreator ~containing:None); - do_nothing () - | `NO -> raise exc - | `CANCEL -> do_nothing()) - in - match guistuff.filenamedata with - | None,None -> handle_without_devel None - | None,Some d -> handle_with_devel d - | Some f,_ -> - match MatitamakeLib.development_for_dir (Filename.dirname f) with - | None -> handle_without_devel (Some f) - | Some d -> handle_with_devel d + | DependenciesParser.UnableToInclude mafilename -> + assert (Pcre.pmatch ~pat:"ma$" mafilename); + check_if_file_is_exists mafilename + | LexiconEngine.IncludedFileNotCompiled (xfilename,mafilename) + | GrafiteEngine.IncludedFileNotCompiled (xfilename,mafilename) as exn -> + assert (Pcre.pmatch ~pat:"ma$" mafilename); + assert (Pcre.pmatch ~pat:"lexicon$" xfilename || + Pcre.pmatch ~pat:"mo$" xfilename ); + (* we know that someone was able to include the .ma, get the baseuri + * but was unable to get the compilation output 'xfilename' *) + match MatitamakeLib.development_for_dir (Filename.dirname mafilename) with + | None -> handle_without_devel mafilename exn + | Some d -> handle_with_devel d xfilename exn ;; let eval_with_engine diff --git a/matita/matitacLib.ml b/matita/matitacLib.ml index d4e67e7a0..93d92c577 100644 --- a/matita/matitacLib.ml +++ b/matita/matitacLib.ml @@ -275,7 +275,7 @@ let main ~mode = end else begin - let baseuri = + let baseuri, _fullpathforfname = DependenciesParser.baseuri_of_script ~include_paths fname in let moo_fname = LibraryMisc.obj_file_of_baseuri diff --git a/matita/matitaclean.ml b/matita/matitaclean.ml index 98d5ffa6b..cf8bf42f4 100644 --- a/matita/matitaclean.ml +++ b/matita/matitaclean.ml @@ -95,7 +95,7 @@ let main () = try UM.buri_of_uri (UM.uri_of_string suri) with UM.IllFormedUri _ -> - let u = + let u,_ = DependenciesParser.baseuri_of_script ~include_paths:[] suri in if String.length u < 5 || String.sub u 0 5 <> "cic:/" then begin HLog.error (sprintf "File %s defines a bad baseuri: %s" diff --git a/matita/matitadep.ml b/matita/matitadep.ml index b951571f3..06a84619e 100644 --- a/matita/matitadep.ml +++ b/matita/matitadep.ml @@ -70,7 +70,7 @@ let main () = Hashtbl.add baseuri_of ma_file uri | DependenciesParser.IncludeDep path -> try - let baseuri = + let baseuri,_ = DependenciesParser.baseuri_of_script ~include_paths path in if not (Http_getter_storage.is_legacy baseuri) then let moo_file = obj_file_of_baseuri false baseuri in