load_thy: avoid reloading of text;
authorwenzelm
Sun Jul 29 22:41:58 2007 +0200 (2007-07-29)
changeset 2406521483400c2ca
parent 24064 7be344a20b6b
child 24066 fb455cb475df
load_thy: avoid reloading of text;
tuned;
src/Pure/Isar/outer_syntax.ML
src/Pure/Thy/thy_load.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Sun Jul 29 22:41:55 2007 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Sun Jul 29 22:41:58 2007 +0200
     1.3 @@ -256,16 +256,15 @@
     1.4        in Toplevel.excursion [Toplevel.empty |> Toplevel.name tr_name |> tr] end
     1.5    end;
     1.6  
     1.7 -fun run_thy dir name time =
     1.8 +fun run_thy dir name pos text time =
     1.9    let
    1.10 -    val master as ((path, _), _) = ThyLoad.check_thy dir name false;
    1.11 -    val text = Source.of_list (Library.untabify (explode (File.read path)));
    1.12 +    val text_src = Source.of_list (Library.untabify text);
    1.13  
    1.14      val _ = Present.init_theory name;
    1.15 -    val _ = Present.verbatim_source name (fn () => Source.exhaust (Symbol.source false text));
    1.16 -    val toks = text
    1.17 +    val _ = Present.verbatim_source name (fn () => Source.exhaust (Symbol.source false text_src));
    1.18 +    val toks = text_src
    1.19        |> Symbol.source false
    1.20 -      |> T.source NONE (K (get_lexicons ())) (Position.path path)
    1.21 +      |> T.source NONE (K (get_lexicons ())) pos
    1.22        |> Source.exhausted;
    1.23      val trs = toks
    1.24        |> toplevel_source false false NONE (K (get_parser ()))
    1.25 @@ -277,15 +276,12 @@
    1.26        |> Buffer.content
    1.27        |> Present.theory_output name);
    1.28      val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
    1.29 -
    1.30 -  in master end;
    1.31 +  in () end;
    1.32  
    1.33 -fun load_thy dir name ml time =
    1.34 -  let
    1.35 -    val master = run_thy dir name time;
    1.36 -    val _ = ML_Context.set_context (SOME (Context.Theory (ThyInfo.get_theory name)));
    1.37 -    val _ = if ml then try_ml_file dir name time else ();
    1.38 -  in master end;
    1.39 +fun load_thy dir name pos text ml time =
    1.40 + (run_thy dir name pos text time;
    1.41 +  ML_Context.set_context (SOME (Context.Theory (ThyInfo.get_theory name)));
    1.42 +  if ml then try_ml_file dir name time else ());
    1.43  
    1.44  in
    1.45  
     2.1 --- a/src/Pure/Thy/thy_load.ML	Sun Jul 29 22:41:55 2007 +0200
     2.2 +++ b/src/Pure/Thy/thy_load.ML	Sun Jul 29 22:41:58 2007 +0200
     2.3 @@ -26,18 +26,17 @@
     2.4    val check_ml: Path.T -> Path.T -> (Path.T * File.ident) option
     2.5    val check_thy: Path.T -> string -> bool -> (Path.T * File.ident) * (Path.T * File.ident) option
     2.6    val deps_thy: Path.T -> string -> bool ->
     2.7 -    ((Path.T * File.ident) * (Path.T * File.ident) option) * (string list * Path.T list)
     2.8 +   {master: (Path.T * File.ident) * (Path.T * File.ident) option,
     2.9 +    text: string list, imports: string list, uses: Path.T list}
    2.10    val load_ml: Path.T -> Path.T -> Path.T * File.ident
    2.11 -  val load_thy: Path.T -> string -> bool -> bool ->
    2.12 -    (Path.T * File.ident) * (Path.T * File.ident) option
    2.13 +  val load_thy: Path.T -> string -> Position.T -> string list -> bool -> bool -> unit
    2.14  end;
    2.15  
    2.16 -(*this backdoor sealed later*)
    2.17  signature PRIVATE_THY_LOAD =
    2.18  sig
    2.19    include THY_LOAD
    2.20 -  val load_thy_fn: (Path.T -> string -> bool -> bool ->
    2.21 -    (Path.T * File.ident) * (Path.T * File.ident) option) ref
    2.22 +  (*this backdoor is sealed later*)
    2.23 +  val load_thy_fn: (Path.T -> string -> Position.T -> string list -> bool -> bool -> unit) ref
    2.24  end;
    2.25  
    2.26  structure ThyLoad: PRIVATE_THY_LOAD =
    2.27 @@ -106,15 +105,17 @@
    2.28  fun deps_thy dir name ml =
    2.29    let
    2.30      val master as ((path, _), _) = check_thy dir name ml;
    2.31 +    val text = explode (File.read path);
    2.32      val (name', imports, uses) =
    2.33 -      ThyHeader.read (Position.path path) (Source.of_string_limited (File.read path));
    2.34 +      ThyHeader.read (Position.path path) (Source.of_list_limited 8000 text);
    2.35      val _ = name = name' orelse
    2.36        error ("Filename " ^ quote (Path.implode (Path.base path)) ^
    2.37          " does not agree with theory name " ^ quote name');
    2.38      val ml_file =
    2.39        if ml andalso is_some (check_file dir (ml_path name))
    2.40        then [ml_path name] else [];
    2.41 -  in (master, (imports, map (Path.explode o #1) uses @ ml_file)) end;
    2.42 +    val uses = map (Path.explode o #1) uses @ ml_file;
    2.43 +  in {master = master, text = text, imports = imports, uses = uses} end;
    2.44  
    2.45  
    2.46  (* load files *)
    2.47 @@ -125,9 +126,9 @@
    2.48    | SOME (path, id) => (ML_Context.use path; (path, id)));
    2.49  
    2.50  (*dependent on outer syntax*)
    2.51 -val load_thy_fn = ref (undefined: Path.T -> string -> bool -> bool ->
    2.52 -  (Path.T * File.ident) * (Path.T * File.ident) option);
    2.53 -fun load_thy dir name ml time = ! load_thy_fn dir name ml time;
    2.54 +val load_thy_fn =
    2.55 +  ref (undefined: Path.T -> string -> Position.T -> string list -> bool -> bool -> unit);
    2.56 +fun load_thy dir name pos text ml time = ! load_thy_fn dir name pos text ml time;
    2.57  
    2.58  end;
    2.59