]> matita.cs.unibo.it Git - helm.git/commitdiff
bugfix to developments:
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 5 Jul 2006 10:40:11 +0000 (10:40 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 5 Jul 2006 10:40:11 +0000 (10:40 +0000)
- 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).

13 files changed:
components/grafite_engine/grafiteEngine.ml
components/grafite_engine/grafiteEngine.mli
components/grafite_parser/dependenciesParser.ml
components/grafite_parser/dependenciesParser.mli
components/grafite_parser/grafiteParser.ml
components/lexicon/lexiconAst.ml
components/lexicon/lexiconAstPp.ml
components/lexicon/lexiconEngine.ml
components/lexicon/lexiconEngine.mli
matita/matitaScript.ml
matita/matitacLib.ml
matita/matitaclean.ml
matita/matitadep.ml

index b066b8ae09cafc5472a21c0bbc16b6a5625d7d21..ad5423b3e77097bbf9f603d2bcf05bcad15b94af 100644 (file)
@@ -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,[]
index b1df5728112816f7cd3114b9cdef3743b46219c3..8363971ae3dad8c6714e5e279c4fc9ee9eaae743 100644 (file)
@@ -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)
index 686caa5b108bbf9e0c971f19c1fecebbe3b8b2b8..74cf0aa774333592b5ed396aab97581a38cd678b 100644 (file)
@@ -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
index 882d45fb8ecaaad0ee31911e8c42133c8ddfa4d5..6a8d2ae212bbfb17495fc0af3be6ce82cfe2c275 100644 (file)
@@ -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
index f99573b30ccf3840f3444f8c509e1b98a751efc0..1a11ec62f0d788e06a15c55d3c3f3453ccb73e7d 100644 (file)
@@ -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
index 50f0061eebb0e894b9a1173dda6538348df14c5e..9fb188d486bfd15cdbd177af975c47e67e4892ff 100644 (file)
@@ -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 *
index 23f0082969aa99d99b6c26b601db5b642694e48d..0b2c9463936671edcb78b812dddeef60760986df 100644 (file)
@@ -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
index 34e314edcd128b13ae820f1e393ea5df5801c49f..1e1fe61c05147eef1dd8df67231df4f18ee3b7b1 100644 (file)
@@ -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
index 8e8b420ba03fabc9354a784b835e7313db38c3b9..00201c9fbf5147f43e3e04565607bf1b01298447 100644 (file)
@@ -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 *)
index 510e736e5cc1896375ec723f2c77ab0c571d0183..5674063e990293482d63d754f50e49d29eaf4998 100644 (file)
@@ -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 <b>" ^ name ^ "</b>.\n\n" ^
+      "<i>Should I compile it and Its dependencies?</i>"
+    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 <b>not</b> handled by a development.\n" ^
+     "All dependencies are automatically solved for a development.\n\n" ^
+     "<i>Do you want to set up a development?</i>"
+    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 <b>" ^ name ^ "</b>.\n\n" ^
-          "<i>Should I compile it and Its dependencies?</i>"
-        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 <b>not</b> handled by a development.\n" ^
-         "All dependencies are automatically solved for a development.\n\n" ^
-         "<i>Do you want to set up a development?</i>"
-        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
index d4e67e7a0ae329de1a46613ceeea57f70ff0b12d..93d92c5771b93da9225062a3cd850de81cd0eb13 100644 (file)
@@ -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 
index 98d5ffa6b540005783b49b573c458bb9018d9eca..cf8bf42f4467f0628e93dad1d2d9b625a87112ec 100644 (file)
@@ -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"
index b951571f3fc85155400553604ad8ddf3aa6190ce..06a84619e798da1cf40e0fbf1d956efbf4db9e21 100644 (file)
@@ -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