merged

--- 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),

--- 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;

--- 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 </" ^ s ^ ">"))
-              (Scan.this_string ("</" ^ s) --| blanks --| $$ ">"))) >> Elem) xs;
+       ($$ "/" -- $$ ">" >> ignored ||
+        $$ ">" |-- parse_content --|
+          !! (err (fn () => "Expected </" ^ implode name ^ ">"))
+              ($$ "<" -- $$ "/" -- 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)

--- 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;