added include' to include everything but preferences (aka aliases)

diff --git a/components/grafite_parser/dependenciesParser.ml b/components/grafite_parser/dependenciesParser.ml
index fc49de60009b78462ebecdbc54ec322cd5fba412..dee9511182333c36d1ff7412f3c6498103e1b475 100644 (file)
--- a/components/grafite_parser/dependenciesParser.ml
+++ b/components/grafite_parser/dependenciesParser.ml
@@ -84,7 +84,7 @@ let baseuri_of_script ~include_paths file =
  if String.length uri < 5 || String.sub uri 0 5 <> "cic:/" then
    HLog.error (file ^ " sets an incorrect baseuri: " ^ buri);
  (try 
-   ignore(Http_getter.resolve uri)
+   ignore(Http_getter.resolve ~writable:false uri)
  with
  | Http_getter_types.Unresolvable_URI _ -> 
      HLog.error (file ^ " sets an unresolvable baseuri: " ^ buri)

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 8848efad6ce3865660fd2b4ed797ab050bf001d9..e83152226f257cb21132fbb3abee6b0f3c271ae7 100644 (file)
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -449,7 +449,10 @@ EXTEND
   ];
   
   include_command: [ [
-      IDENT "include" ; path = QSTRING -> loc,path
+      IDENT "include" ; path = QSTRING -> 
+        loc,path,LexiconAst.WithPreferences
+    | IDENT "include'" ; path = QSTRING -> 
+        loc,path,LexiconAst.WithoutPreferences
    ]];
 
   grafite_command: [ [
@@ -528,11 +531,11 @@ EXTEND
        fun ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
     | com = comment ->
        fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
-    | (iloc,fname) = include_command ; SYMBOL "."  ->
+    | (iloc,fname,mode) = include_command ; SYMBOL "."  ->
        fun ~include_paths status ->
         let path = DependenciesParser.baseuri_of_script ~include_paths fname in
         let status =
-         LexiconEngine.eval_command status (LexiconAst.Include (iloc,path))
+         LexiconEngine.eval_command status (LexiconAst.Include (iloc,path,mode))
         in
          status,
           LSome

diff --git a/components/lexicon/lexiconAst.ml b/components/lexicon/lexiconAst.ml
index aed4b0b152365ea8ee0e191f96ab1aabfbee5bda..50f0061eebb0e894b9a1173dda6538348df14c5e 100644 (file)
--- a/components/lexicon/lexiconAst.ml
+++ b/components/lexicon/lexiconAst.ml
@@ -38,8 +38,10 @@ type alias_spec =
  * marshalling *)
 let magic = 5
 
+type inclusion_mode = WithPreferences | WithoutPreferences (* aka aliases *)
+
 type command =
-  | Include of loc * string
+  | Include of loc * string * inclusion_mode
   | 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 e49a66f607b7a305463b592ff9962564c8374269..4b20958aa084fc3b672243229355fa2d25b47edb 100644 (file)
--- a/components/lexicon/lexiconAstPp.ml
+++ b/components/lexicon/lexiconAstPp.ml
@@ -75,7 +75,11 @@ let pp_notation dir_opt l1_pattern assoc prec l2_pattern =
     (pp_l2_pattern l2_pattern)
     
 let pp_command = function
-  | Include (_,path) -> "include " ^ path
+  | Include (_,path,mode) -> 
+      if mode = WithPreferences then
+        "include " ^ path
+      else
+        "include' " ^ path
   | Alias (_,s) -> pp_alias s
   | Interpretation (_, dsc, (symbol, arg_patterns), cic_appl_pattern) ->
       pp_interpretation dsc symbol arg_patterns cic_appl_pattern

diff --git a/components/lexicon/lexiconEngine.ml b/components/lexicon/lexiconEngine.ml
index d3a8954ff7479be5978ad73d62126d51f8238f28..34e314edcd128b13ae820f1e393ea5df5801c49f 100644 (file)
--- a/components/lexicon/lexiconEngine.ml
+++ b/components/lexicon/lexiconEngine.ml
@@ -72,44 +72,50 @@ let add_metadata new_metadata status =
   else
     status
 
-let set_proof_aliases status new_aliases =
- let commands_of_aliases =
-   List.map
-    (fun alias -> LexiconAst.Alias (HExtlib.dummy_floc, alias))
- in
- let deps_of_aliases =
-   HExtlib.filter_map
-    (function
-    | LexiconAst.Ident_alias (_, suri) ->
-        let buri = UriManager.buri_of_uri (UriManager.uri_of_string suri) in
-        Some (LibraryNoDb.Dependency buri)
-    | _ -> None)
- in
- let aliases =
-  List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc)
-   status.aliases new_aliases in
- let multi_aliases =
-  List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.cons d c acc)
-   status.multi_aliases new_aliases in
- let new_status =
-   { status with multi_aliases = multi_aliases ; aliases = aliases}
- in
- if new_aliases = [] then
-   new_status
+let set_proof_aliases mode status new_aliases =
+ if mode = LexiconAst.WithoutPreferences then
+   status 
  else
-   let aliases = 
-     DisambiguatePp.aliases_of_domain_and_codomain_items_list new_aliases
+   let commands_of_aliases =
+     List.map
+      (fun alias -> LexiconAst.Alias (HExtlib.dummy_floc, alias))
    in
-   let status = add_lexicon_content (commands_of_aliases aliases) new_status in
-   let status = add_metadata (deps_of_aliases aliases) status in
-   status
+   let deps_of_aliases =
+     HExtlib.filter_map
+      (function
+      | LexiconAst.Ident_alias (_, suri) ->
+          let buri = UriManager.buri_of_uri (UriManager.uri_of_string suri) in
+          Some (LibraryNoDb.Dependency buri)
+      | _ -> None)
+   in
+   let aliases =
+    List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc)
+     status.aliases new_aliases in
+   let multi_aliases =
+    List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.cons d c acc)
+     status.multi_aliases new_aliases in
+   let new_status =
+     { status with multi_aliases = multi_aliases ; aliases = aliases}
+   in
+   if new_aliases = [] then
+     new_status
+   else
+     let aliases = 
+       DisambiguatePp.aliases_of_domain_and_codomain_items_list new_aliases
+     in
+     let status = 
+       add_lexicon_content (commands_of_aliases aliases) new_status 
+     in
+     let status = add_metadata (deps_of_aliases aliases) status in
+     status
+
 
-let rec eval_command status cmd =
+let rec eval_command ?(mode=LexiconAst.WithPreferences) status cmd =
  let notation_ids' = CicNotation.process_notation cmd in
  let status =
    { status with notation_ids = notation_ids' @ status.notation_ids } in
   match cmd with
-  | LexiconAst.Include (loc, baseuri) ->
+  | LexiconAst.Include (loc, baseuri, mode) ->
      let lexiconpath_rw, lexiconpath_r = 
        LibraryMisc.lexicon_file_of_baseuri 
          ~must_exist:false ~writable:true ~baseuri,
@@ -122,7 +128,7 @@ let rec eval_command status cmd =
           raise (IncludedFileNotCompiled lexiconpath_rw)
      in
      let lexicon = LexiconMarshal.load_lexicon lexiconpath in
-     let status = List.fold_left eval_command status lexicon in
+     let status = List.fold_left (eval_command ~mode) status lexicon in
       if Helm_registry.get_bool "db.nodb" then
        let metadatapath_rw, metadatapath_r = 
          LibraryMisc.metadata_file_of_baseuri 
@@ -153,7 +159,7 @@ let rec eval_command status cmd =
          [DisambiguateTypes.Num instance,
           DisambiguateChoices.lookup_num_by_dsc desc]
      in
-      set_proof_aliases status diff
+      set_proof_aliases mode status diff
   | LexiconAst.Interpretation (_, dsc, (symbol, _), cic_appl_pattern) as stm ->
       let status = add_lexicon_content [stm] status in
       let uris =
@@ -165,8 +171,12 @@ let rec eval_command status cmd =
        [DisambiguateTypes.Symbol (symbol, 0),
          DisambiguateChoices.lookup_symbol_by_dsc symbol dsc]
       in
-      let status = set_proof_aliases status diff in
+      let status = set_proof_aliases mode status diff in
       let status = add_metadata uris status in
       status
   | LexiconAst.Notation _ as stm -> add_lexicon_content [stm] status
 
+let eval_command = eval_command ?mode:None
+
+let set_proof_aliases  = set_proof_aliases LexiconAst.WithPreferences
+