# HG changeset patch # User wenzelm # Date 1311456839 -7200 # Node ID 521de6ab277a29751ba2fe15740c70cd3e49bff3 # Parent 3b69f057ef2e4e9e0f9df6d67dd3be11a5e43560# Parent 318ca53e3fbb6b5e483eb321bd580d0588ad6073 merged diff -r 3b69f057ef2e -r 521de6ab277a src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Sat Jul 23 20:05:28 2011 +0200 +++ b/src/Pure/Concurrent/future.ML Sat Jul 23 23:33:59 2011 +0200 @@ -208,7 +208,7 @@ fold (fn job => fn ok => job valid andalso ok) jobs true) ()); val _ = Multithreading.tracing 2 (fn () => let - val s = Task_Queue.str_of_task task; + val s = Task_Queue.str_of_task_groups task; fun micros time = string_of_int (Time.toNanoseconds time div 1000); val (run, wait, deps) = Task_Queue.timing_of_task task; in "TASK " ^ s ^ " " ^ micros run ^ " " ^ micros wait ^ " (" ^ commas deps ^ ")" end); @@ -253,7 +253,7 @@ fun worker_loop name = (case SYNCHRONIZED name (fn () => worker_next ()) of NONE => () - | SOME work => (execute work; worker_loop name)); + | SOME work => (Exn.capture Multithreading.interrupted (); execute work; worker_loop name)); fun worker_start name = (*requires SYNCHRONIZED*) Unsynchronized.change workers (cons (Simple_Thread.fork false (fn () => worker_loop name), diff -r 3b69f057ef2e -r 521de6ab277a src/Pure/Concurrent/task_queue.ML --- a/src/Pure/Concurrent/task_queue.ML Sat Jul 23 20:05:28 2011 +0200 +++ b/src/Pure/Concurrent/task_queue.ML Sat Jul 23 23:33:59 2011 +0200 @@ -14,12 +14,14 @@ val is_canceled: group -> bool val group_status: group -> exn list val str_of_group: group -> string + val str_of_groups: group -> string type task val dummy_task: unit -> task val group_of_task: task -> group val name_of_task: task -> string val pri_of_task: task -> int val str_of_task: task -> string + val str_of_task_groups: task -> string val timing_of_task: task -> Time.time * Time.time * string list val running: task -> (unit -> 'a) -> 'a val joining: task -> (unit -> 'a) -> 'a @@ -64,8 +66,8 @@ fun group_id (Group {id, ...}) = id; fun eq_group (group1, group2) = group_id group1 = group_id group2; -fun group_ancestry f (Group {parent = NONE, id, ...}) a = f id a - | group_ancestry f (Group {parent = SOME group, id, ...}) a = group_ancestry f group (f id a); +fun fold_groups f (g as Group {parent = NONE, ...}) a = f g a + | fold_groups f (g as Group {parent = SOME group, ...}) a = fold_groups f group (f g a); (* group status *) @@ -87,6 +89,9 @@ fun str_of_group group = (is_canceled group ? enclose "(" ")") (string_of_int (group_id group)); +fun str_of_groups group = + space_implode "/" (map str_of_group (rev (fold_groups cons group []))); + end; @@ -114,9 +119,12 @@ fun group_of_task (Task {group, ...}) = group; fun name_of_task (Task {name, ...}) = name; fun pri_of_task (Task {pri, ...}) = the_default 0 pri; + fun str_of_task (Task {name, id, ...}) = if name = "" then string_of_int id else string_of_int id ^ " (" ^ name ^ ")"; +fun str_of_task_groups task = str_of_task task ^ " in " ^ str_of_groups (group_of_task task); + fun timing_of_task (Task {timing, ...}) = Synchronized.value timing; fun update_timing update (Task {timing, ...}) e = @@ -263,7 +271,7 @@ fun finish task (Queue {groups, jobs}) = let val group = group_of_task task; - val groups' = group_ancestry (fn gid => del_task (gid, task)) group groups; + val groups' = fold_groups (fn g => del_task (group_id g, task)) group groups; val jobs' = Task_Graph.del_node task jobs; val maximal = null (Task_Graph.imm_succs jobs task); in (maximal, make_queue groups' jobs') end; @@ -274,14 +282,14 @@ fun enqueue_passive group abort (Queue {groups, jobs}) = let val task = new_task group "passive" NONE; - val groups' = group_ancestry (fn gid => add_task (gid, task)) group groups; + val groups' = fold_groups (fn g => add_task (group_id g, task)) group groups; val jobs' = jobs |> Task_Graph.new_node (task, Passive abort); in (task, make_queue groups' jobs') end; fun enqueue name group deps pri job (Queue {groups, jobs}) = let val task = new_task group name (SOME pri); - val groups' = group_ancestry (fn gid => add_task (gid, task)) group groups; + val groups' = fold_groups (fn g => add_task (group_id g, task)) group groups; val jobs' = jobs |> Task_Graph.new_node (task, Job [job]) |> fold (add_job task) deps; diff -r 3b69f057ef2e -r 521de6ab277a src/Pure/General/xml.ML --- a/src/Pure/General/xml.ML Sat Jul 23 20:05:28 2011 +0200 +++ b/src/Pure/General/xml.ML Sat Jul 23 23:33:59 2011 +0200 @@ -183,6 +183,10 @@ val parse_optional_text = Scan.optional (parse_chars >> (single o Text)) []; +fun name_start_char c = Symbol.is_ascii_letter c orelse c = ":" orelse c = "_"; +fun name_char c = name_start_char c orelse Symbol.is_ascii_digit c orelse c = "-" orelse c = "."; +val parse_name = Scan.one name_start_char ::: Scan.many name_char; + in val parse_comments = @@ -200,13 +204,14 @@ @@@ parse_optional_text) >> flat)) xs and parse_element xs = - ($$ "<" |-- Symbol.scan_id -- - Scan.repeat (blanks |-- parse_att) --| blanks :-- (fn (s, _) => + ($$ "<" |-- parse_name -- Scan.repeat (blanks |-- parse_att) --| blanks :-- + (fn (name, _) => !! (err (fn () => "Expected > or />")) - (Scan.this_string "/>" >> ignored - || $$ ">" |-- parse_content --| - !! (err (fn () => "Expected ")) - (Scan.this_string (""))) >> Elem) xs; + ($$ "/" -- $$ ">" >> ignored || + $$ ">" |-- parse_content --| + !! (err (fn () => "Expected ")) + ($$ "<" -- $$ "/" -- Scan.this name -- blanks -- $$ ">"))) + >> (fn ((name, atts), body) => Elem ((implode name, atts), body))) xs; val parse_document = (Scan.repeat parse_misc -- Scan.option parse_doctype -- Scan.repeat parse_misc) diff -r 3b69f057ef2e -r 521de6ab277a src/Pure/term_sharing.ML --- a/src/Pure/term_sharing.ML Sat Jul 23 20:05:28 2011 +0200 +++ b/src/Pure/term_sharing.ML Sat Jul 23 23:33:59 2011 +0200 @@ -57,7 +57,13 @@ val _ = Unsynchronized.change terms (Syntax_Termtab.update (tm', ())); in tm' end); - in (typ, term) end; + fun check eq f x = + let val x' = f x in + if eq (x, x') then x' + else raise Fail "Something is utterly wrong" + end; + + in (check (op =) typ, check (op =) term) end; val typs = map o #1 o init; val terms = map o #2 o init;