--- a/src/Pure/Concurrent/future.ML Thu Jul 22 12:07:30 2010 +0200
+++ b/src/Pure/Concurrent/future.ML Thu Jul 22 16:53:00 2010 +0200
@@ -3,6 +3,7 @@
Future values, see also
http://www4.in.tum.de/~wenzelm/papers/parallel-isabelle.pdf
+http://www4.in.tum.de/~wenzelm/papers/parallel-ml.pdf
Notes:
--- a/src/Pure/Concurrent/single_assignment.ML Thu Jul 22 12:07:30 2010 +0200
+++ b/src/Pure/Concurrent/single_assignment.ML Thu Jul 22 16:53:00 2010 +0200
@@ -31,7 +31,7 @@
fun peek (Var {var, ...}) = SingleAssignment.savalue var;
-fun await (v as Var {name, lock, cond, var}) =
+fun await (v as Var {name, lock, cond, ...}) =
Simple_Thread.synchronized name lock (fn () =>
let
fun wait () =
--- a/src/Pure/General/source.ML Thu Jul 22 12:07:30 2010 +0200
+++ b/src/Pure/General/source.ML Thu Jul 22 16:53:00 2010 +0200
@@ -16,9 +16,9 @@
val map_filter: ('a -> 'b option) -> ('a, 'c) source -> ('b, ('a, 'c) source) source
val filter: ('a -> bool) -> ('a, 'b) source -> ('a, ('a, 'b) source) source
val of_list: 'a list -> ('a, 'a list) source
- val of_list_limited: int -> 'a list -> ('a, 'a list) source
+ val exhausted: ('a, 'b) source -> ('a, 'a list) source
val of_string: string -> (string, string list) source
- val exhausted: ('a, 'b) source -> ('a, 'a list) source
+ val of_string_limited: int -> string -> (string, substring) source
val tty: (string, unit) source
val source': 'a -> 'b Scan.stopper -> ('a * 'b list -> 'c list * ('a * 'b list)) ->
(bool * (string -> 'a * 'b list -> 'c list * ('a * 'b list))) option ->
@@ -101,11 +101,21 @@
(* list source *)
fun of_list xs = make_source [] xs default_prompt (fn _ => fn xs => (xs, []));
-fun of_list_limited n xs = make_source [] xs default_prompt (fn _ => chop n);
+
+fun exhausted src = of_list (exhaust src);
+
+
+(* string source *)
val of_string = of_list o explode;
-fun exhausted src = of_list (exhaust src);
+fun of_string_limited limit str =
+ make_source [] (Substring.full str) default_prompt
+ (fn _ => fn s =>
+ let
+ val (s1, s2) = Substring.splitAt (s, Int.min (Substring.size s, limit));
+ val cs = map String.str (Substring.explode s1);
+ in (cs, s2) end);
(* stream source *)
--- a/src/Pure/Isar/outer_syntax.ML Thu Jul 22 12:07:30 2010 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Thu Jul 22 16:53:00 2010 +0200
@@ -31,7 +31,7 @@
type isar
val isar: bool -> isar
val prepare_command: Position.T -> string -> Toplevel.transition
- val load_thy: string -> Position.T -> string list -> unit -> unit
+ val load_thy: string -> Position.T -> string -> unit -> unit
end;
structure Outer_Syntax: OUTER_SYNTAX =
@@ -275,11 +275,11 @@
val _ = Present.init_theory name;
- val toks = Source.exhausted (Thy_Syntax.token_source lexs pos (Source.of_list text));
+ val toks = Source.exhausted (Thy_Syntax.token_source lexs pos (Source.of_string text));
val spans = Source.exhaust (Thy_Syntax.span_source toks);
val _ = List.app Thy_Syntax.report_span spans;
val units = Source.exhaust (Thy_Syntax.unit_source (Source.of_list spans))
- |> maps (prepare_unit commands);
+ |> Par_List.map (prepare_unit commands) |> flat;
val _ = Present.theory_source name
(fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
--- a/src/Pure/Isar/toplevel.ML Thu Jul 22 12:07:30 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML Thu Jul 22 16:53:00 2010 +0200
@@ -578,7 +578,9 @@
(* post-transition hooks *)
-local val hooks = Unsynchronized.ref ([]: (transition -> state -> state -> unit) list) in
+local
+ val hooks = Unsynchronized.ref ([]: (transition -> state -> state -> unit) list);
+in
fun add_hook f = CRITICAL (fn () => Unsynchronized.change hooks (cons f));
fun get_hooks () = ! hooks;
@@ -597,9 +599,10 @@
fun do_profiling f x = profile (! profiling) f x;
val (result, status) =
- state |> (apply_trans int trans
- |> (if ! profiling > 0 andalso not no_timing then do_profiling else I)
- |> (if ! profiling > 0 orelse ! timing andalso not no_timing then do_timing else I));
+ state |>
+ (apply_trans int trans
+ |> (! profiling > 0 andalso not no_timing) ? do_profiling
+ |> (! profiling > 0 orelse ! timing andalso not no_timing) ? do_timing);
val _ = if int andalso not (! quiet) andalso print then print_state false result else ();
in (result, Option.map (fn UNDEF => type_error tr state | exn => exn) status) end);
@@ -626,7 +629,7 @@
(* managed execution *)
-fun run_command thy_name (tr as Transition {print, ...}) st =
+fun run_command thy_name tr st =
(case
(case init_of tr of
SOME name => Exn.capture (fn () => Thy_Load.check_name thy_name name) ()
--- a/src/Pure/Thy/thy_info.ML Thu Jul 22 12:07:30 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML Thu Jul 22 16:53:00 2010 +0200
@@ -85,7 +85,7 @@
type deps =
{update_time: int, (*symbolic time of update; negative value means outdated*)
master: (Path.T * File.ident) option, (*master dependencies for thy file*)
- text: string list, (*source text for thy*)
+ text: string, (*source text for thy*)
parents: string list, (*source specification of parents (partially qualified)*)
(*auxiliary files: source path, physical path + identifier*)
files: (Path.T * (Path.T * File.ident) option) list};
@@ -105,10 +105,8 @@
fun base_name s = Path.implode (Path.base (Path.explode s));
-type thy = deps option * theory option;
-
local
- val database = Unsynchronized.ref (Graph.empty: thy Graph.T);
+ val database = Unsynchronized.ref (Graph.empty: (deps option * theory option) Graph.T);
in
fun get_thys () = ! database;
fun change_thys f = CRITICAL (fn () => Unsynchronized.change database f);
@@ -329,11 +327,13 @@
fun load_thy upd_time initiators name =
let
val _ = priority ("Loading theory " ^ quote name ^ required_by " " initiators);
+ fun corrupted () = error (loader_msg "corrupted dependency information" [name]);
val (pos, text, _) =
(case get_deps name of
- SOME {master = SOME (master_path, _), text as _ :: _, files, ...} =>
- (Path.position master_path, text, files)
- | _ => error (loader_msg "corrupted dependency information" [name]));
+ SOME {master = SOME (master_path, _), text, files, ...} =>
+ if text = "" then corrupted ()
+ else (Path.position master_path, text, files)
+ | _ => corrupted ());
val _ = touch_thy name;
val _ = CRITICAL (fn () =>
change_deps name (Option.map (fn {master, text, parents, files, ...} =>
@@ -343,7 +343,7 @@
CRITICAL (fn () =>
(change_deps name
(Option.map (fn {update_time, master, parents, files, ...} =>
- make_deps update_time master [] parents files));
+ make_deps update_time master "" parents files));
perform Update name));
in after_load end;
@@ -419,9 +419,11 @@
fun check_ml master (src_path, info) =
let val info' =
- (case info of NONE => NONE
+ (case info of
+ NONE => NONE
| SOME (_, id) =>
- (case Thy_Load.check_ml (master_dir master) src_path of NONE => NONE
+ (case Thy_Load.check_ml (master_dir master) src_path of
+ NONE => NONE
| SOME (path', id') => if id <> id' then NONE else SOME (path', id')))
in (src_path, info') end;
@@ -451,7 +453,7 @@
end);
fun read_text (SOME {update_time, master = master as SOME (path, _), text = _, parents, files}) =
- SOME (make_deps update_time master (explode (File.read path)) parents files);
+ SOME (make_deps update_time master (File.read path) parents files);
in
@@ -521,7 +523,7 @@
val deps =
if known_thy name then get_deps name
- else init_deps NONE [] parents (map #1 uses);
+ else init_deps NONE "" parents (map #1 uses);
val _ = change_thys (new_deps name parent_names (deps, NONE));
val update_time = (case deps of NONE => 0 | SOME {update_time, ...} => update_time);
@@ -558,7 +560,7 @@
in
CRITICAL (fn () =>
(change_deps name (Option.map
- (fn {parents, files, ...} => make_deps upd_time (SOME master) [] parents files));
+ (fn {parents, files, ...} => make_deps upd_time (SOME master) "" parents files));
perform Update name))
end;
--- a/src/Pure/Thy/thy_load.ML Thu Jul 22 12:07:30 2010 +0200
+++ b/src/Pure/Thy/thy_load.ML Thu Jul 22 16:53:00 2010 +0200
@@ -27,7 +27,7 @@
val check_thy: Path.T -> string -> Path.T * File.ident
val check_name: string -> string -> unit
val deps_thy: Path.T -> string ->
- {master: Path.T * File.ident, text: string list, imports: string list, uses: Path.T list}
+ {master: Path.T * File.ident, text: string, imports: string list, uses: Path.T list}
val load_ml: Path.T -> Path.T -> Path.T * File.ident
end;
@@ -114,9 +114,9 @@
fun deps_thy dir name =
let
val master as (path, _) = check_thy dir name;
- val text = explode (File.read path);
+ val text = File.read path;
val (name', imports, uses) =
- Thy_Header.read (Path.position path) (Source.of_list_limited 8000 text);
+ Thy_Header.read (Path.position path) (Source.of_string_limited 8000 text);
val _ = check_name name name';
val uses = map (Path.explode o #1) uses;
in {master = master, text = text, imports = imports, uses = uses} end;