more standard Thy_Load.check_thy for Pure.thy, relying on its header;
authorwenzelm
Tue Aug 21 21:48:32 2012 +0200 (2012-08-21)
changeset 48876157dd47032e0
parent 48875 b629f037a0cb
child 48877 51659a3819a7
more standard Thy_Load.check_thy for Pure.thy, relying on its header;
pass uses and keywords from Thy_Load.check_thy to Thy_Info.load_thy;
clarified 'ML_file' wrt. Thy_Load.require/provide, which is also relevant for Thy_Load.all_current;
src/Pure/ROOT.ML
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_load.ML
     1.1 --- a/src/Pure/ROOT.ML	Tue Aug 21 21:25:45 2012 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Tue Aug 21 21:48:32 2012 +0200
     1.3 @@ -324,12 +324,17 @@
     1.4  val _ =
     1.5    Outer_Syntax.command
     1.6      (("ML_file", Keyword.tag_ml Keyword.thy_load), Position.none) "ML text from file"
     1.7 -    (Thy_Load.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy =>
     1.8 -      let val (_, [(txt, pos)]) = files (Context.theory_of gthy) in
     1.9 -        gthy
    1.10 -        |> ML_Context.exec (fn () => ML_Context.eval_text true pos txt)
    1.11 -        |> Local_Theory.propagate_ml_env
    1.12 -      end)));
    1.13 +    (Scan.ahead Parse.path -- Thy_Load.parse_files "ML_file"
    1.14 +      >> (fn (src_path, files) => Toplevel.generic_theory (fn gthy =>
    1.15 +        let
    1.16 +          val (dir, [(txt, pos)]) = files (Context.theory_of gthy);
    1.17 +          val provide = Thy_Load.provide (src_path, (File.full_path dir src_path, SHA1.digest txt));
    1.18 +        in
    1.19 +          gthy
    1.20 +          |> ML_Context.exec (fn () => ML_Context.eval_text true pos txt)
    1.21 +          |> Local_Theory.propagate_ml_env
    1.22 +          |> Context.mapping provide (Local_Theory.background_theory provide)
    1.23 +        end)));
    1.24  
    1.25  Unsynchronized.setmp Multithreading.max_threads 1
    1.26    use_thy "Pure";
     2.1 --- a/src/Pure/Thy/thy_info.ML	Tue Aug 21 21:25:45 2012 +0200
     2.2 +++ b/src/Pure/Thy/thy_info.ML	Tue Aug 21 21:48:32 2012 +0200
     2.3 @@ -220,7 +220,7 @@
     2.4  fun required_by _ [] = ""
     2.5    | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
     2.6  
     2.7 -fun load_thy initiators update_time deps text name parents =
     2.8 +fun load_thy initiators update_time deps text name uses keywords parents =
     2.9    let
    2.10      val _ = kill_thy name;
    2.11      val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);
    2.12 @@ -228,7 +228,6 @@
    2.13      val {master = (thy_path, _), imports} = deps;
    2.14      val dir = Path.dir thy_path;
    2.15      val pos = Path.position thy_path;
    2.16 -    val {uses, keywords, ...} = Thy_Header.read pos text;
    2.17      val header = Thy_Header.make name imports keywords uses;
    2.18  
    2.19      val (theory, present) =
    2.20 @@ -239,21 +238,21 @@
    2.21  
    2.22  fun check_deps base_keywords dir name =
    2.23    (case lookup_deps name of
    2.24 -    SOME NONE => (true, NONE, get_imports name, [])
    2.25 +    SOME NONE => (true, NONE, get_imports name, [], [])
    2.26    | NONE =>
    2.27 -      let val {master, text, imports, keywords, ...} = Thy_Load.check_thy base_keywords dir name
    2.28 -      in (false, SOME (make_deps master imports, text), imports, keywords) end
    2.29 +      let val {master, text, imports, keywords, uses} = Thy_Load.check_thy base_keywords dir name
    2.30 +      in (false, SOME (make_deps master imports, text), imports, uses, keywords) end
    2.31    | SOME (SOME {master, ...}) =>
    2.32        let
    2.33 -        val {master = master', text = text', imports = imports', keywords, ...} =
    2.34 -          Thy_Load.check_thy base_keywords dir name;
    2.35 +        val {master = master', text = text', imports = imports', uses = uses', keywords = keywords'}
    2.36 +          = Thy_Load.check_thy base_keywords dir name;
    2.37          val deps' = SOME (make_deps master' imports', text');
    2.38          val current =
    2.39            #2 master = #2 master' andalso
    2.40              (case lookup_theory name of
    2.41                NONE => false
    2.42              | SOME theory => Thy_Load.all_current theory);
    2.43 -      in (current, deps', imports', keywords) end);
    2.44 +      in (current, deps', imports', uses', keywords') end);
    2.45  
    2.46  in
    2.47  
    2.48 @@ -271,7 +270,7 @@
    2.49            val dir' = Path.append dir (Path.dir path);
    2.50            val _ = member (op =) initiators name andalso error (cycle_msg initiators);
    2.51  
    2.52 -          val (current, deps, imports, keywords) = check_deps base_keywords dir' name
    2.53 +          val (current, deps, imports, uses, keywords) = check_deps base_keywords dir' name
    2.54              handle ERROR msg => cat_error msg
    2.55                (loader_msg "the error(s) above occurred while examining theory" [name] ^
    2.56                  required_by "\n" initiators);
    2.57 @@ -288,8 +287,10 @@
    2.58                (case deps of
    2.59                  NONE => raise Fail "Malformed deps"
    2.60                | SOME (dep, text) =>
    2.61 -                  let val update_time = serial ()
    2.62 -                  in Task (parents, load_thy initiators update_time dep text name) end);
    2.63 +                  let
    2.64 +                    val update_time = serial ();
    2.65 +                    val load = load_thy initiators update_time dep text name uses keywords;
    2.66 +                  in Task (parents, load) end);
    2.67  
    2.68            val base_keywords'' = keywords @ base_keywords';
    2.69            val tasks'' = new_entry name parents task tasks';
     3.1 --- a/src/Pure/Thy/thy_load.ML	Tue Aug 21 21:25:45 2012 +0200
     3.2 +++ b/src/Pure/Thy/thy_load.ML	Tue Aug 21 21:48:32 2012 +0200
     3.3 @@ -11,9 +11,9 @@
     3.4    val provide: Path.T * (Path.T * SHA1.digest) -> theory -> theory
     3.5    val check_file: Path.T -> Path.T -> Path.T
     3.6    val thy_path: Path.T -> Path.T
     3.7 -  val check_thy: (string * Keyword.T option) list -> Path.T -> string ->
     3.8 +  val check_thy: Thy_Header.keywords -> Path.T -> string ->
     3.9     {master: Path.T * SHA1.digest, text: string, imports: string list,
    3.10 -    uses: (Path.T * bool) list, keywords: (string * Keyword.T option) list}
    3.11 +    uses: (Path.T * bool) list, keywords: Thy_Header.keywords}
    3.12    val load_file: theory -> Path.T -> (Path.T * SHA1.digest) * string
    3.13    val use_file: Path.T -> theory -> string * theory
    3.14    val loaded_files: theory -> Path.T list
    3.15 @@ -157,28 +157,23 @@
    3.16  
    3.17  val thy_path = Path.ext "thy";
    3.18  
    3.19 -fun check_thy base_keywords dir name =
    3.20 +fun check_thy base_keywords dir thy_name =
    3.21    let
    3.22 -    val path = thy_path (Path.basic name);
    3.23 +    val path = thy_path (Path.basic thy_name);
    3.24      val master_file = check_file dir path;
    3.25      val text = File.read master_file;
    3.26 -    val (name', imports, uses, more_keywords) =
    3.27 -      if name = Context.PureN then (Context.PureN, [], [], [])
    3.28 -      else
    3.29 -        let
    3.30 -          val {name, imports, uses, keywords} = Thy_Header.read (Path.position master_file) text;
    3.31 -          val more_keywords = map (apsnd (Option.map Keyword.spec)) keywords;
    3.32 -          val syntax =
    3.33 -            Keyword.get_keywords ()
    3.34 -            |> fold Keyword.define_keywords base_keywords
    3.35 -            |> fold Keyword.define_keywords more_keywords;
    3.36 -          val more_uses = map (rpair false) (find_files syntax text);
    3.37 -        in (name, imports, uses @ more_uses, more_keywords) end;
    3.38 -    val _ = name <> name' andalso
    3.39 -      error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name');
    3.40 +
    3.41 +    val {name, imports, uses, keywords} = Thy_Header.read (Path.position master_file) text;
    3.42 +    val _ = thy_name <> name andalso
    3.43 +      error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name);
    3.44 +
    3.45 +    val syntax =
    3.46 +      fold (Keyword.define_keywords o apsnd (Option.map Keyword.spec))
    3.47 +        (keywords @ base_keywords) (Keyword.get_keywords ());
    3.48 +    val more_uses = map (rpair false) (find_files syntax text);
    3.49    in
    3.50     {master = (master_file, SHA1.digest text), text = text,
    3.51 -    imports = imports, uses = uses, keywords = more_keywords}
    3.52 +    imports = imports, uses = uses @ more_uses, keywords = keywords}
    3.53    end;
    3.54  
    3.55