From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 11 May 2006 11:27:44 +0000 (+0000)
Subject: Bugs fixed:
X-Git-Tag: make_still_working~7381
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f7f2a793b445a052138cd3df377a9e417f6e37c4;p=helm.git

Bugs fixed:
 * the dependency parser no longer fails when an incomplete "include" or "set"
   are met
 * ask_and_save_moo is now performed more lazily and some bugs have been fixed
---

diff --git a/helm/software/components/grafite_parser/dependenciesParser.ml b/helm/software/components/grafite_parser/dependenciesParser.ml
index 69a28c962..686caa5b1 100644
--- a/helm/software/components/grafite_parser/dependenciesParser.ml
+++ b/helm/software/components/grafite_parser/dependenciesParser.ml
@@ -43,6 +43,7 @@ let parse_dependencies lexbuf =
     CicNotationLexer.level2_ast_lexer.Token.tok_func (Obj.magic lexbuf)
   in
   let rec parse acc = 
+   try
     (parser
     | [< '("URI", u) >] ->
         parse (UriDep (UriManager.uri_of_string u) :: acc)
@@ -53,6 +54,8 @@ let parse_dependencies lexbuf =
     | [< '("EOI", _) >] -> acc
     | [< 'tok >] -> parse acc
     | [<  >] -> acc) tok_stream
+   with
+    Stream.Error _ -> parse acc
   in
   List.rev (parse [])
 
diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 04b86d0b7..1f170cb91 100644
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -70,47 +70,55 @@ let clean_current_baseuri grafite_status =
     with GrafiteTypes.Option_error _ -> ()
 
 let ask_and_save_moo_if_needed parent fname lexicon_status grafite_status = 
-  let baseuri = DependenciesParser.baseuri_of_script ~include_paths:[] fname in
-  let moo_fname = 
-    LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri ~writable:true in
-  let save () =
-    let metadata_fname =
-     LibraryMisc.metadata_file_of_baseuri 
-       ~must_exist:false ~baseuri ~writable:true in
-    let lexicon_fname =
-     LibraryMisc.lexicon_file_of_baseuri 
-       ~must_exist:false ~baseuri ~writable:true
-    in
-     GrafiteMarshal.save_moo moo_fname
-      grafite_status.GrafiteTypes.moo_content_rev;
-     LibraryNoDb.save_metadata metadata_fname
-      lexicon_status.LexiconEngine.metadata;
-     LexiconMarshal.save_lexicon lexicon_fname
-      lexicon_status.LexiconEngine.lexicon_content_rev
+  let baseuri =
+   try Some (GrafiteTypes.get_string_option grafite_status "baseuri")
+   with GrafiteTypes.Option_error _ -> None
   in
   if (MatitaScript.current ())#eos &&
-     grafite_status.GrafiteTypes.proof_status = GrafiteTypes.No_proof
+     grafite_status.GrafiteTypes.proof_status = GrafiteTypes.No_proof &&
+     baseuri <> None
   then
-    begin
-      let rc = 
-        MatitaGtkMisc.ask_confirmation
-        ~title:"A .moo can be generated"
-        ~message:(Printf.sprintf 
-          "%s can be generated for %s.\n<i>Should I generate it?</i>"
-          (Filename.basename moo_fname) (Filename.basename fname))
-        ~parent ()
-      in
-      let b = 
-        match rc with 
-        | `YES -> true 
-        | `NO -> false 
-        | `CANCEL -> raise MatitaTypes.Cancel 
+   begin
+    let baseuri = match baseuri with Some b -> b | None -> assert false in
+    let moo_fname = 
+     LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri
+      ~writable:true in
+    let save () =
+      let metadata_fname =
+       LibraryMisc.metadata_file_of_baseuri 
+         ~must_exist:false ~baseuri ~writable:true in
+      let lexicon_fname =
+       LibraryMisc.lexicon_file_of_baseuri 
+         ~must_exist:false ~baseuri ~writable:true
       in
-      if b then
-          save ()
-      else
-        clean_current_baseuri grafite_status
-    end
+       GrafiteMarshal.save_moo moo_fname
+        grafite_status.GrafiteTypes.moo_content_rev;
+       LibraryNoDb.save_metadata metadata_fname
+        lexicon_status.LexiconEngine.metadata;
+       LexiconMarshal.save_lexicon lexicon_fname
+        lexicon_status.LexiconEngine.lexicon_content_rev
+    in
+     begin
+       let rc = 
+         MatitaGtkMisc.ask_confirmation
+         ~title:"A .moo can be generated"
+         ~message:(Printf.sprintf 
+           "%s can be generated for %s.\n<i>Should I generate it?</i>"
+           (Filename.basename moo_fname) (Filename.basename fname))
+         ~parent ()
+       in
+       let b = 
+         match rc with 
+         | `YES -> true 
+         | `NO -> false 
+         | `CANCEL -> raise MatitaTypes.Cancel 
+       in
+       if b then
+           save ()
+       else
+         clean_current_baseuri grafite_status
+     end
+   end
   else
     clean_current_baseuri grafite_status 
     
diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 07a7cbd2e..510e736e5 100644
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -772,9 +772,10 @@ object (self)
       in
       match st with
       | GrafiteParser.LSome (GrafiteAst.Comment (loc,_)) -> 
-          let _,parsed_text_length = 
-            MatitaGtkMisc.utf8_parsed_text s loc 
-          in
+          let _,parsed_text_length = MatitaGtkMisc.utf8_parsed_text s loc in
+          (* CSC: why +1 in the following lines ???? *)
+          let parsed_text_length = parsed_text_length + 1 in
+prerr_endline ("## " ^ string_of_int parsed_text_length);
           let remain_len = String.length s - parsed_text_length in
           let next = String.sub s parsed_text_length remain_len in
           is_there_only_comments lexicon_status next
@@ -784,6 +785,7 @@ object (self)
     try
       is_there_only_comments self#lexicon_status self#getFuture
     with 
+    | LexiconEngine.IncludedFileNotCompiled _
     | HExtlib.Localized _
     | CicNotationParser.Parse_error _ -> false
     | Margin | End_of_file -> true