1.1 --- a/src/Pure/Concurrent/future.ML	Sat Jul 23 20:05:28 2011 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Sat Jul 23 23:33:59 2011 +0200
     1.3 @@ -208,7 +208,7 @@
     1.4            fold (fn job => fn ok => job valid andalso ok) jobs true) ());
     1.5      val _ = Multithreading.tracing 2 (fn () =>
     1.6        let
     1.7 -        val s = Task_Queue.str_of_task task;
     1.8 +        val s = Task_Queue.str_of_task_groups task;
     1.9          fun micros time = string_of_int (Time.toNanoseconds time div 1000);
    1.10          val (run, wait, deps) = Task_Queue.timing_of_task task;
    1.11        in "TASK " ^ s ^ " " ^ micros run ^ " " ^ micros wait ^ " (" ^ commas deps ^ ")" end);
    1.12 @@ -253,7 +253,7 @@
    1.13  fun worker_loop name =
    1.14    (case SYNCHRONIZED name (fn () => worker_next ()) of
    1.15      NONE => ()
    1.16 -  | SOME work => (execute work; worker_loop name));
    1.17 +  | SOME work => (Exn.capture Multithreading.interrupted (); execute work; worker_loop name));
    1.18  
    1.19  fun worker_start name = (*requires SYNCHRONIZED*)
    1.20    Unsynchronized.change workers (cons (Simple_Thread.fork false (fn () => worker_loop name),

     2.1 --- a/src/Pure/Concurrent/task_queue.ML	Sat Jul 23 20:05:28 2011 +0200
     2.2 +++ b/src/Pure/Concurrent/task_queue.ML	Sat Jul 23 23:33:59 2011 +0200
     2.3 @@ -14,12 +14,14 @@
     2.4    val is_canceled: group -> bool
     2.5    val group_status: group -> exn list
     2.6    val str_of_group: group -> string
     2.7 +  val str_of_groups: group -> string
     2.8    type task
     2.9    val dummy_task: unit -> task
    2.10    val group_of_task: task -> group
    2.11    val name_of_task: task -> string
    2.12    val pri_of_task: task -> int
    2.13    val str_of_task: task -> string
    2.14 +  val str_of_task_groups: task -> string
    2.15    val timing_of_task: task -> Time.time * Time.time * string list
    2.16    val running: task -> (unit -> 'a) -> 'a
    2.17    val joining: task -> (unit -> 'a) -> 'a
    2.18 @@ -64,8 +66,8 @@
    2.19  fun group_id (Group {id, ...}) = id;
    2.20  fun eq_group (group1, group2) = group_id group1 = group_id group2;
    2.21  
    2.22 -fun group_ancestry f (Group {parent = NONE, id, ...}) a = f id a
    2.23 -  | group_ancestry f (Group {parent = SOME group, id, ...}) a = group_ancestry f group (f id a);
    2.24 +fun fold_groups f (g as Group {parent = NONE, ...}) a = f g a
    2.25 +  | fold_groups f (g as Group {parent = SOME group, ...}) a = fold_groups f group (f g a);
    2.26  
    2.27  
    2.28  (* group status *)
    2.29 @@ -87,6 +89,9 @@
    2.30  fun str_of_group group =
    2.31    (is_canceled group ? enclose "(" ")") (string_of_int (group_id group));
    2.32  
    2.33 +fun str_of_groups group =
    2.34 +  space_implode "/" (map str_of_group (rev (fold_groups cons group [])));
    2.35 +
    2.36  end;
    2.37  
    2.38  
    2.39 @@ -114,9 +119,12 @@
    2.40  fun group_of_task (Task {group, ...}) = group;
    2.41  fun name_of_task (Task {name, ...}) = name;
    2.42  fun pri_of_task (Task {pri, ...}) = the_default 0 pri;
    2.43 +
    2.44  fun str_of_task (Task {name, id, ...}) =
    2.45    if name = "" then string_of_int id else string_of_int id ^ " (" ^ name ^ ")";
    2.46  
    2.47 +fun str_of_task_groups task = str_of_task task ^ " in " ^ str_of_groups (group_of_task task);
    2.48 +
    2.49  fun timing_of_task (Task {timing, ...}) = Synchronized.value timing;
    2.50  
    2.51  fun update_timing update (Task {timing, ...}) e =
    2.52 @@ -263,7 +271,7 @@
    2.53  fun finish task (Queue {groups, jobs}) =
    2.54    let
    2.55      val group = group_of_task task;
    2.56 -    val groups' = group_ancestry (fn gid => del_task (gid, task)) group groups;
    2.57 +    val groups' = fold_groups (fn g => del_task (group_id g, task)) group groups;
    2.58      val jobs' = Task_Graph.del_node task jobs;
    2.59      val maximal = null (Task_Graph.imm_succs jobs task);
    2.60    in (maximal, make_queue groups' jobs') end;
    2.61 @@ -274,14 +282,14 @@
    2.62  fun enqueue_passive group abort (Queue {groups, jobs}) =
    2.63    let
    2.64      val task = new_task group "passive" NONE;
    2.65 -    val groups' = group_ancestry (fn gid => add_task (gid, task)) group groups;
    2.66 +    val groups' = fold_groups (fn g => add_task (group_id g, task)) group groups;
    2.67      val jobs' = jobs |> Task_Graph.new_node (task, Passive abort);
    2.68    in (task, make_queue groups' jobs') end;
    2.69  
    2.70  fun enqueue name group deps pri job (Queue {groups, jobs}) =
    2.71    let
    2.72      val task = new_task group name (SOME pri);
    2.73 -    val groups' = group_ancestry (fn gid => add_task (gid, task)) group groups;
    2.74 +    val groups' = fold_groups (fn g => add_task (group_id g, task)) group groups;
    2.75      val jobs' = jobs
    2.76        |> Task_Graph.new_node (task, Job [job])
    2.77        |> fold (add_job task) deps;

     3.1 --- a/src/Pure/General/xml.ML	Sat Jul 23 20:05:28 2011 +0200
     3.2 +++ b/src/Pure/General/xml.ML	Sat Jul 23 23:33:59 2011 +0200
     3.3 @@ -183,6 +183,10 @@
     3.4  val parse_optional_text =
     3.5    Scan.optional (parse_chars >> (single o Text)) [];
     3.6  
     3.7 +fun name_start_char c = Symbol.is_ascii_letter c orelse c = ":" orelse c = "_";
     3.8 +fun name_char c = name_start_char c orelse Symbol.is_ascii_digit c orelse c = "-" orelse c = ".";
     3.9 +val parse_name = Scan.one name_start_char ::: Scan.many name_char;
    3.10 +
    3.11  in
    3.12  
    3.13  val parse_comments =
    3.14 @@ -200,13 +204,14 @@
    3.15        @@@ parse_optional_text) >> flat)) xs
    3.16  
    3.17  and parse_element xs =
    3.18 -  ($$ "<" |-- Symbol.scan_id --
    3.19 -    Scan.repeat (blanks |-- parse_att) --| blanks :-- (fn (s, _) =>
    3.20 +  ($$ "<" |-- parse_name -- Scan.repeat (blanks |-- parse_att) --| blanks :--
    3.21 +    (fn (name, _) =>
    3.22        !! (err (fn () => "Expected > or />"))
    3.23 -        (Scan.this_string "/>" >> ignored
    3.24 -         || $$ ">" |-- parse_content --|
    3.25 -            !! (err (fn () => "Expected </" ^ s ^ ">"))
    3.26 -              (Scan.this_string ("</" ^ s) --| blanks --| $$ ">"))) >> Elem) xs;
    3.27 +       ($$ "/" -- $$ ">" >> ignored ||
    3.28 +        $$ ">" |-- parse_content --|
    3.29 +          !! (err (fn () => "Expected </" ^ implode name ^ ">"))
    3.30 +              ($$ "<" -- $$ "/" -- Scan.this name -- blanks -- $$ ">")))
    3.31 +    >> (fn ((name, atts), body) => Elem ((implode name, atts), body))) xs;
    3.32  
    3.33  val parse_document =
    3.34    (Scan.repeat parse_misc -- Scan.option parse_doctype -- Scan.repeat parse_misc)

     4.1 --- a/src/Pure/term_sharing.ML	Sat Jul 23 20:05:28 2011 +0200
     4.2 +++ b/src/Pure/term_sharing.ML	Sat Jul 23 23:33:59 2011 +0200
     4.3 @@ -57,7 +57,13 @@
     4.4              val _ = Unsynchronized.change terms (Syntax_Termtab.update (tm', ()));
     4.5            in tm' end);
     4.6  
     4.7 -  in (typ, term) end;
     4.8 +    fun check eq f x =
     4.9 +      let val x' = f x in
    4.10 +        if eq (x, x') then x'
    4.11 +        else raise Fail "Something is utterly wrong"
    4.12 +      end;
    4.13 +
    4.14 +  in (check (op =) typ, check (op =) term) end;
    4.15  
    4.16  val typs = map o #1 o init;
    4.17  val terms = map o #2 o init;