# HG changeset patch # User wenzelm # Date 1279810380 -7200 # Node ID b8ca89c45086a8ff76c6d7d1bcf3a96a71da96eb # Parent d00a3f47b6072e9e07a6f6da261a4c15b419e6a7# Parent f18c4bc8b02869584fe677d60a4adeee805a5bbb merged diff -r d00a3f47b607 -r b8ca89c45086 src/Pure/Concurrent/future.ML --- 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: diff -r d00a3f47b607 -r b8ca89c45086 src/Pure/Concurrent/single_assignment.ML --- 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 () = diff -r d00a3f47b607 -r b8ca89c45086 src/Pure/General/source.ML --- 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 *) diff -r d00a3f47b607 -r b8ca89c45086 src/Pure/Isar/outer_syntax.ML --- 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); diff -r d00a3f47b607 -r b8ca89c45086 src/Pure/Isar/toplevel.ML --- 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) () diff -r d00a3f47b607 -r b8ca89c45086 src/Pure/Thy/thy_info.ML --- 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; diff -r d00a3f47b607 -r b8ca89c45086 src/Pure/Thy/thy_load.ML --- 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;