# HG changeset patch
# User wenzelm
# Date 1281523833 -7200
# Node ID 01d2ef471ffe979e741f5f35a0183e0f3eb98088
# Parent  6daf896bca5ea53870c5070b27d406a6a54f29d0# Parent  d31a345695425f6415d4a98506ae5188d0921fb9
merged, resolving conflict in src/Pure/IsaMakefile concerning General/xml_data.ML;

diff -r 6daf896bca5e -r 01d2ef471ffe bin/isabelle-process
--- a/bin/isabelle-process	Wed Aug 11 12:04:06 2010 +0200
+++ b/bin/isabelle-process	Wed Aug 11 12:50:33 2010 +0200
@@ -29,8 +29,8 @@
   echo "    -I           startup Isar interaction mode"
   echo "    -P           startup Proof General interaction mode"
   echo "    -S           secure mode -- disallow critical operations"
+  echo "    -W IN:OUT    startup process wrapper, with input/output fifos"
   echo "    -X           startup PGIP interaction mode"
-  echo "    -W OUTPUT    startup process wrapper, with messages going to OUTPUT stream"
   echo "    -e MLTEXT    pass MLTEXT to the ML session"
   echo "    -f           pass 'Session.finish();' to the ML session"
   echo "    -m MODE      add print mode for output"
@@ -61,7 +61,7 @@
 ISAR=false
 PROOFGENERAL=""
 SECURE=""
-WRAPPER_OUTPUT=""
+WRAPPER_FIFOS=""
 PGIP=""
 MLTEXT=""
 MODES=""
@@ -82,7 +82,7 @@
       SECURE=true
       ;;
     W)
-      WRAPPER_OUTPUT="$OPTARG"
+      WRAPPER_FIFOS="$OPTARG"
       ;;
     X)
       PGIP=true
@@ -212,9 +212,13 @@
 [ -n "$SECURE" ] && MLTEXT="$MLTEXT Secure.set_secure ();"
 
 NICE="nice"
-if [ -n "$WRAPPER_OUTPUT" ]; then
-  [ "$WRAPPER_OUTPUT" = "-" -o -p "$WRAPPER_OUTPUT" ] || fail "Bad named pipe: $WRAPPER_OUTPUT"
-  MLTEXT="$MLTEXT; Isabelle_Process.init \"$WRAPPER_OUTPUT\";"
+
+if [ -n "$WRAPPER_FIFOS" ]; then
+  splitarray ":" "$WRAPPER_FIFOS"; FIFOS=("${SPLITARRAY[@]}")
+  [ "${#FIFOS[@]}" -eq 2 ] || fail "Expected IN:OUT fifo specification"
+  [ -p "${FIFOS[0]}" ] || fail "Bad input fifo: ${FIFOS[0]}"
+  [ -p "${FIFOS[1]}" ] || fail "Bad output fifo: ${FIFOS[1]}"
+  MLTEXT="$MLTEXT; Isabelle_Process.init \"${FIFOS[0]}\" \"${FIFOS[1]}\";"
 elif [ -n "$PGIP" ]; then
   MLTEXT="$MLTEXT; ProofGeneralPgip.init_pgip $ISAR;"
 elif [ -n "$PROOFGENERAL" ]; then
diff -r 6daf896bca5e -r 01d2ef471ffe doc-src/System/Thy/Basics.thy
--- a/doc-src/System/Thy/Basics.thy	Wed Aug 11 12:04:06 2010 +0200
+++ b/doc-src/System/Thy/Basics.thy	Wed Aug 11 12:50:33 2010 +0200
@@ -331,7 +331,7 @@
     -I           startup Isar interaction mode
     -P           startup Proof General interaction mode
     -S           secure mode -- disallow critical operations
-    -W OUTPUT    startup process wrapper, with messages going to OUTPUT stream
+    -W IN:OUT    startup process wrapper, with input/output fifos
     -X           startup PGIP interaction mode
     -e MLTEXT    pass MLTEXT to the ML session
     -f           pass 'Session.finish();' to the ML session
@@ -406,12 +406,13 @@
   interaction mode on startup, instead of the primitive ML top-level.
   The @{verbatim "-P"} option configures the top-level loop for
   interaction with the Proof General user interface, and the
-  @{verbatim "-X"} option enables XML-based PGIP communication.  The
-  @{verbatim "-W"} option makes Isabelle enter a special process
-  wrapper for interaction via an external program; the protocol is a
-  stripped-down version of Proof General the interaction mode, see
-  also @{"file" "~~/src/Pure/System/isabelle_process.ML"} and @{"file"
-  "~~/src/Pure/System/isabelle_process.scala"}.
+  @{verbatim "-X"} option enables XML-based PGIP communication.
+
+  \medskip The @{verbatim "-W"} option makes Isabelle enter a special
+  process wrapper for interaction via the Isabelle/Scala layer, see
+  also @{"file" "~~/src/Pure/System/isabelle_process.scala"}.  The
+  protocol between the ML and JVM process is private to the
+  implementation.
 
   \medskip The @{verbatim "-S"} option makes the Isabelle process more
   secure by disabling some critical operations, notably runtime
diff -r 6daf896bca5e -r 01d2ef471ffe doc-src/System/Thy/document/Basics.tex
--- a/doc-src/System/Thy/document/Basics.tex	Wed Aug 11 12:04:06 2010 +0200
+++ b/doc-src/System/Thy/document/Basics.tex	Wed Aug 11 12:50:33 2010 +0200
@@ -344,7 +344,7 @@
     -I           startup Isar interaction mode
     -P           startup Proof General interaction mode
     -S           secure mode -- disallow critical operations
-    -W OUTPUT    startup process wrapper, with messages going to OUTPUT stream
+    -W IN:OUT    startup process wrapper, with input/output fifos
     -X           startup PGIP interaction mode
     -e MLTEXT    pass MLTEXT to the ML session
     -f           pass 'Session.finish();' to the ML session
@@ -419,11 +419,13 @@
   interaction mode on startup, instead of the primitive ML top-level.
   The \verb|-P| option configures the top-level loop for
   interaction with the Proof General user interface, and the
-  \verb|-X| option enables XML-based PGIP communication.  The
-  \verb|-W| option makes Isabelle enter a special process
-  wrapper for interaction via an external program; the protocol is a
-  stripped-down version of Proof General the interaction mode, see
-  also \hyperlink{file.~~/src/Pure/System/isabelle-process.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}System{\isacharslash}isabelle{\isacharunderscore}process{\isachardot}ML}}}} and \hyperlink{file.~~/src/Pure/System/isabelle-process.scala}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}System{\isacharslash}isabelle{\isacharunderscore}process{\isachardot}scala}}}}.
+  \verb|-X| option enables XML-based PGIP communication.
+
+  \medskip The \verb|-W| option makes Isabelle enter a special
+  process wrapper for interaction via the Isabelle/Scala layer, see
+  also \hyperlink{file.~~/src/Pure/System/isabelle-process.scala}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}System{\isacharslash}isabelle{\isacharunderscore}process{\isachardot}scala}}}}.  The
+  protocol between the ML and JVM process is private to the
+  implementation.
 
   \medskip The \verb|-S| option makes the Isabelle process more
   secure by disabling some critical operations, notably runtime
diff -r 6daf896bca5e -r 01d2ef471ffe lib/Tools/mkfifo
--- a/lib/Tools/mkfifo	Wed Aug 11 12:04:06 2010 +0200
+++ b/lib/Tools/mkfifo	Wed Aug 11 12:50:33 2010 +0200
@@ -28,6 +28,8 @@
 
 [ "$#" != 0 ] && usage
 
+#FIXME potential race condition wrt. future processes with same pid
 FIFO="/tmp/isabelle-fifo$$"
-mkfifo -m 600 "$FIFO" || fail "Failed to create named pipe $FIFO"
+
+mkfifo -m 600 "$FIFO" || fail "Failed to create fifo: $FIFO"
 echo "$FIFO"
diff -r 6daf896bca5e -r 01d2ef471ffe lib/scripts/raw_dump
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/raw_dump	Wed Aug 11 12:50:33 2010 +0200
@@ -0,0 +1,56 @@
+#!/usr/bin/env perl
+#
+# Author: Makarius
+#
+# raw_dump - direct copy without extra buffering
+#
+
+use warnings;
+use strict;
+
+use IO::File;
+
+
+# args
+
+my ($input, $output) = @ARGV;
+
+
+# prepare files
+
+my $infile;
+my $outfile;
+
+if ($input eq "-") { $infile = *STDIN; }
+else {
+  $infile = new IO::File $input, "r";
+  defined $infile || die $!;
+}
+
+if ($output eq "-") { $outfile = *STDOUT; }
+else {
+  $outfile = new IO::File $output, "w";
+  defined $outfile || die $!;
+}
+
+binmode $infile;
+binmode $outfile;
+
+
+# main loop
+
+my $chunk;
+while ((sysread $infile, $chunk, 65536), length $chunk > 0) {
+  my $end = length $chunk;
+  my $offset = 0;
+  while ($offset < $end) {
+    $offset += syswrite $outfile, $chunk, $end - $offset, $offset;
+  }
+}
+
+
+# cleanup
+
+undef $infile;
+undef $outfile;
+
diff -r 6daf896bca5e -r 01d2ef471ffe src/HOL/Matrix/ComputeFloat.thy
--- a/src/HOL/Matrix/ComputeFloat.thy	Wed Aug 11 12:04:06 2010 +0200
+++ b/src/HOL/Matrix/ComputeFloat.thy	Wed Aug 11 12:50:33 2010 +0200
@@ -9,13 +9,11 @@
 uses "~~/src/Tools/float.ML" ("~~/src/HOL/Tools/float_arith.ML")
 begin
 
-definition
-  pow2 :: "int \<Rightarrow> real" where
-  "pow2 a = (if (0 <= a) then (2^(nat a)) else (inverse (2^(nat (-a)))))"
+definition pow2 :: "int \<Rightarrow> real"
+  where "pow2 a = (if (0 <= a) then (2^(nat a)) else (inverse (2^(nat (-a)))))"
 
-definition
-  float :: "int * int \<Rightarrow> real" where
-  "float x = real (fst x) * pow2 (snd x)"
+definition float :: "int * int \<Rightarrow> real"
+  where "float x = real (fst x) * pow2 (snd x)"
 
 lemma pow2_0[simp]: "pow2 0 = 1"
 by (simp add: pow2_def)
@@ -99,13 +97,11 @@
 lemma "float (a, e) + float (b, e) = float (a + b, e)"
 by (simp add: float_def algebra_simps)
 
-definition
-  int_of_real :: "real \<Rightarrow> int" where
-  "int_of_real x = (SOME y. real y = x)"
+definition int_of_real :: "real \<Rightarrow> int"
+  where "int_of_real x = (SOME y. real y = x)"
 
-definition
-  real_is_int :: "real \<Rightarrow> bool" where
-  "real_is_int x = (EX (u::int). x = real u)"
+definition real_is_int :: "real \<Rightarrow> bool"
+  where "real_is_int x = (EX (u::int). x = real u)"
 
 lemma real_is_int_def2: "real_is_int x = (x = real (int_of_real x))"
 by (auto simp add: real_is_int_def int_of_real_def)
@@ -345,15 +341,11 @@
 lemma float_mult_r0: "x * float (0, e) = float (0, 0)"
   by (simp add: float_def)
 
-definition 
-  lbound :: "real \<Rightarrow> real"
-where
-  "lbound x = min 0 x"
+definition lbound :: "real \<Rightarrow> real"
+  where "lbound x = min 0 x"
 
-definition
-  ubound :: "real \<Rightarrow> real"
-where
-  "ubound x = max 0 x"
+definition ubound :: "real \<Rightarrow> real"
+  where "ubound x = max 0 x"
 
 lemma lbound: "lbound x \<le> x"   
   by (simp add: lbound_def)
diff -r 6daf896bca5e -r 01d2ef471ffe src/HOL/Matrix/ComputeHOL.thy
--- a/src/HOL/Matrix/ComputeHOL.thy	Wed Aug 11 12:04:06 2010 +0200
+++ b/src/HOL/Matrix/ComputeHOL.thy	Wed Aug 11 12:50:33 2010 +0200
@@ -62,10 +62,8 @@
 lemma compute_None_None_eq: "(None = None) = True" by auto
 lemma compute_Some_Some_eq: "(Some x = Some y) = (x = y)" by auto
 
-definition
-   option_case_compute :: "'b option \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
-where
-   "option_case_compute opt a f = option_case a f opt"
+definition option_case_compute :: "'b option \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
+  where "option_case_compute opt a f = option_case a f opt"
 
 lemma option_case_compute: "option_case = (\<lambda> a f opt. option_case_compute opt a f)"
   by (simp add: option_case_compute_def)
@@ -96,10 +94,8 @@
 
 (*** compute_list_case ***)
 
-definition
-  list_case_compute :: "'b list \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'b list \<Rightarrow> 'a) \<Rightarrow> 'a"
-where
-  "list_case_compute l a f = list_case a f l"
+definition list_case_compute :: "'b list \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'b list \<Rightarrow> 'a) \<Rightarrow> 'a"
+  where "list_case_compute l a f = list_case a f l"
 
 lemma list_case_compute: "list_case = (\<lambda> (a::'a) f (l::'b list). list_case_compute l a f)"
   apply (rule ext)+
diff -r 6daf896bca5e -r 01d2ef471ffe src/HOL/Matrix/ComputeNumeral.thy
--- a/src/HOL/Matrix/ComputeNumeral.thy	Wed Aug 11 12:04:06 2010 +0200
+++ b/src/HOL/Matrix/ComputeNumeral.thy	Wed Aug 11 12:50:33 2010 +0200
@@ -20,8 +20,7 @@
 lemmas bitiszero = iszero1 iszero2 iszero3 iszero4
 
 (* lezero for bit strings *)
-definition
-  "lezero x == (x \<le> 0)"
+definition "lezero x \<longleftrightarrow> x \<le> 0"
 lemma lezero1: "lezero Int.Pls = True" unfolding Int.Pls_def lezero_def by auto
 lemma lezero2: "lezero Int.Min = True" unfolding Int.Min_def lezero_def by auto
 lemma lezero3: "lezero (Int.Bit0 x) = lezero x" unfolding Int.Bit0_def lezero_def by auto
@@ -60,8 +59,7 @@
 
 lemmas bitarith = bitnorm bitiszero bitneg bitlezero biteq bitless bitle bitsucc bitpred bituminus bitadd bitmul 
 
-definition
-  "nat_norm_number_of (x::nat) == x"
+definition "nat_norm_number_of (x::nat) = x"
 
 lemma nat_norm_number_of: "nat_norm_number_of (number_of w) = (if lezero w then 0 else number_of w)"
   apply (simp add: nat_norm_number_of_def)
@@ -104,8 +102,7 @@
   by (auto simp add: number_of_is_id lezero_def nat_number_of_def)
 
 fun natfac :: "nat \<Rightarrow> nat"
-where
-   "natfac n = (if n = 0 then 1 else n * (natfac (n - 1)))"
+  where "natfac n = (if n = 0 then 1 else n * (natfac (n - 1)))"
 
 lemmas compute_natarith = bitarith natnorm natsuc natadd natsub natmul nateq natless natle natfac.simps
 
diff -r 6daf896bca5e -r 01d2ef471ffe src/HOL/Matrix/Matrix.thy
--- a/src/HOL/Matrix/Matrix.thy	Wed Aug 11 12:04:06 2010 +0200
+++ b/src/HOL/Matrix/Matrix.thy	Wed Aug 11 12:50:33 2010 +0200
@@ -367,15 +367,15 @@
 definition zero_closed :: "(('a::zero) \<Rightarrow> ('b::zero) \<Rightarrow> ('c::zero)) \<Rightarrow> bool" where
   "zero_closed f == (!x. f x 0 = 0) & (!y. f 0 y = 0)"
 
-consts foldseq :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a"
-primrec
+primrec foldseq :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a"
+where
   "foldseq f s 0 = s 0"
-  "foldseq f s (Suc n) = f (s 0) (foldseq f (% k. s(Suc k)) n)"
+| "foldseq f s (Suc n) = f (s 0) (foldseq f (% k. s(Suc k)) n)"
 
-consts foldseq_transposed ::  "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a"
-primrec
+primrec foldseq_transposed ::  "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a"
+where
   "foldseq_transposed f s 0 = s 0"
-  "foldseq_transposed f s (Suc n) = f (foldseq_transposed f s n) (s (Suc n))"
+| "foldseq_transposed f s (Suc n) = f (foldseq_transposed f s n) (s (Suc n))"
 
 lemma foldseq_assoc : "associative f \<Longrightarrow> foldseq f = foldseq_transposed f"
 proof -
diff -r 6daf896bca5e -r 01d2ef471ffe src/HOL/Matrix/SparseMatrix.thy
--- a/src/HOL/Matrix/SparseMatrix.thy	Wed Aug 11 12:04:06 2010 +0200
+++ b/src/HOL/Matrix/SparseMatrix.thy	Wed Aug 11 12:50:33 2010 +0200
@@ -10,11 +10,11 @@
   'a spvec = "(nat * 'a) list"
   'a spmat = "('a spvec) spvec"
 
-definition sparse_row_vector :: "('a::ab_group_add) spvec \<Rightarrow> 'a matrix" where
-  sparse_row_vector_def: "sparse_row_vector arr = foldl (% m x. m + (singleton_matrix 0 (fst x) (snd x))) 0 arr"
+definition sparse_row_vector :: "('a::ab_group_add) spvec \<Rightarrow> 'a matrix"
+  where "sparse_row_vector arr = foldl (% m x. m + (singleton_matrix 0 (fst x) (snd x))) 0 arr"
 
-definition sparse_row_matrix :: "('a::ab_group_add) spmat \<Rightarrow> 'a matrix" where
-  sparse_row_matrix_def: "sparse_row_matrix arr = foldl (% m r. m + (move_matrix (sparse_row_vector (snd r)) (int (fst r)) 0)) 0 arr"
+definition sparse_row_matrix :: "('a::ab_group_add) spmat \<Rightarrow> 'a matrix"
+  where "sparse_row_matrix arr = foldl (% m r. m + (move_matrix (sparse_row_vector (snd r)) (int (fst r)) 0)) 0 arr"
 
 code_datatype sparse_row_vector sparse_row_matrix
 
@@ -57,13 +57,15 @@
   apply (auto simp add: sparse_row_matrix_cons)
   done
 
-primrec sorted_spvec :: "'a spvec \<Rightarrow> bool" where
+primrec sorted_spvec :: "'a spvec \<Rightarrow> bool"
+where
   "sorted_spvec [] = True"
-  | sorted_spvec_step: "sorted_spvec (a#as) = (case as of [] \<Rightarrow> True | b#bs \<Rightarrow> ((fst a < fst b) & (sorted_spvec as)))" 
+| sorted_spvec_step: "sorted_spvec (a#as) = (case as of [] \<Rightarrow> True | b#bs \<Rightarrow> ((fst a < fst b) & (sorted_spvec as)))" 
 
-primrec sorted_spmat :: "'a spmat \<Rightarrow> bool" where
+primrec sorted_spmat :: "'a spmat \<Rightarrow> bool"
+where
   "sorted_spmat [] = True"
-  | "sorted_spmat (a#as) = ((sorted_spvec (snd a)) & (sorted_spmat as))"
+| "sorted_spmat (a#as) = ((sorted_spvec (snd a)) & (sorted_spmat as))"
 
 declare sorted_spvec.simps [simp del]
 
@@ -99,13 +101,15 @@
   apply (simp add: sparse_row_matrix_cons neg_def)
   done
 
-primrec minus_spvec :: "('a::ab_group_add) spvec \<Rightarrow> 'a spvec" where
+primrec minus_spvec :: "('a::ab_group_add) spvec \<Rightarrow> 'a spvec"
+where
   "minus_spvec [] = []"
-  | "minus_spvec (a#as) = (fst a, -(snd a))#(minus_spvec as)"
+| "minus_spvec (a#as) = (fst a, -(snd a))#(minus_spvec as)"
 
-primrec abs_spvec ::  "('a::lattice_ab_group_add_abs) spvec \<Rightarrow> 'a spvec" where
+primrec abs_spvec :: "('a::lattice_ab_group_add_abs) spvec \<Rightarrow> 'a spvec"
+where
   "abs_spvec [] = []"
-  | "abs_spvec (a#as) = (fst a, abs (snd a))#(abs_spvec as)"
+| "abs_spvec (a#as) = (fst a, abs (snd a))#(abs_spvec as)"
 
 lemma sparse_row_vector_minus: 
   "sparse_row_vector (minus_spvec v) = - (sparse_row_vector v)"
@@ -150,8 +154,7 @@
   apply (simp add: sorted_spvec.simps split:list.split_asm)
   done
   
-definition
-  "smult_spvec y = map (% a. (fst a, y * snd a))"  
+definition "smult_spvec y = map (% a. (fst a, y * snd a))"  
 
 lemma smult_spvec_empty[simp]: "smult_spvec y [] = []"
   by (simp add: smult_spvec_def)
@@ -159,10 +162,11 @@
 lemma smult_spvec_cons: "smult_spvec y (a#arr) = (fst a, y * (snd a)) # (smult_spvec y arr)"
   by (simp add: smult_spvec_def)
 
-fun addmult_spvec :: "('a::ring) \<Rightarrow> 'a spvec \<Rightarrow> 'a spvec \<Rightarrow> 'a spvec" where
-  "addmult_spvec y arr [] = arr" |
-  "addmult_spvec y [] brr = smult_spvec y brr" |
-  "addmult_spvec y ((i,a)#arr) ((j,b)#brr) = (
+fun addmult_spvec :: "('a::ring) \<Rightarrow> 'a spvec \<Rightarrow> 'a spvec \<Rightarrow> 'a spvec"
+where
+  "addmult_spvec y arr [] = arr"
+| "addmult_spvec y [] brr = smult_spvec y brr"
+| "addmult_spvec y ((i,a)#arr) ((j,b)#brr) = (
     if i < j then ((i,a)#(addmult_spvec y arr ((j,b)#brr))) 
     else (if (j < i) then ((j, y * b)#(addmult_spvec y ((i,a)#arr) brr))
     else ((i, a + y*b)#(addmult_spvec y arr brr))))"
@@ -235,11 +239,12 @@
   apply (simp_all add: sorted_spvec_addmult_spvec_helper3)
   done
 
-fun mult_spvec_spmat :: "('a::lattice_ring) spvec \<Rightarrow> 'a spvec \<Rightarrow> 'a spmat  \<Rightarrow> 'a spvec" where
+fun mult_spvec_spmat :: "('a::lattice_ring) spvec \<Rightarrow> 'a spvec \<Rightarrow> 'a spmat  \<Rightarrow> 'a spvec"
+where
 (* recdef mult_spvec_spmat "measure (% (c, arr, brr). (length arr) + (length brr))" *)
-  "mult_spvec_spmat c [] brr = c" |
-  "mult_spvec_spmat c arr [] = c" |
-  "mult_spvec_spmat c ((i,a)#arr) ((j,b)#brr) = (
+  "mult_spvec_spmat c [] brr = c"
+| "mult_spvec_spmat c arr [] = c"
+| "mult_spvec_spmat c ((i,a)#arr) ((j,b)#brr) = (
      if (i < j) then mult_spvec_spmat c arr ((j,b)#brr)
      else if (j < i) then mult_spvec_spmat c ((i,a)#arr) brr 
      else mult_spvec_spmat (addmult_spvec a c b) arr brr)"
@@ -342,12 +347,10 @@
   apply (simp_all add: sorted_addmult_spvec)
   done
 
-consts 
-  mult_spmat :: "('a::lattice_ring) spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat"
-
-primrec 
+primrec mult_spmat :: "('a::lattice_ring) spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat"
+where
   "mult_spmat [] A = []"
-  "mult_spmat (a#as) A = (fst a, mult_spvec_spmat [] (snd a) A)#(mult_spmat as A)"
+| "mult_spmat (a#as) A = (fst a, mult_spvec_spmat [] (snd a) A)#(mult_spmat as A)"
 
 lemma sparse_row_mult_spmat: 
   "sorted_spmat A \<Longrightarrow> sorted_spvec B \<Longrightarrow>
@@ -372,12 +375,13 @@
   done
 
 
-fun add_spvec :: "('a::lattice_ab_group_add) spvec \<Rightarrow> 'a spvec \<Rightarrow> 'a spvec" where
+fun add_spvec :: "('a::lattice_ab_group_add) spvec \<Rightarrow> 'a spvec \<Rightarrow> 'a spvec"
+where
 (* "measure (% (a, b). length a + (length b))" *)
-  "add_spvec arr [] = arr" |
-  "add_spvec [] brr = brr" |
-  "add_spvec ((i,a)#arr) ((j,b)#brr) = (
-  if i < j then (i,a)#(add_spvec arr ((j,b)#brr)) 
+  "add_spvec arr [] = arr"
+| "add_spvec [] brr = brr"
+| "add_spvec ((i,a)#arr) ((j,b)#brr) = (
+     if i < j then (i,a)#(add_spvec arr ((j,b)#brr)) 
      else if (j < i) then (j,b) # add_spvec ((i,a)#arr) brr
      else (i, a+b) # add_spvec arr brr)"
 
@@ -389,17 +393,18 @@
   apply (simp_all add: singleton_matrix_add)
   done
 
-fun add_spmat :: "('a::lattice_ab_group_add) spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat" where
+fun add_spmat :: "('a::lattice_ab_group_add) spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat"
+where
 (* "measure (% (A,B). (length A)+(length B))" *)
-  "add_spmat [] bs = bs" |
-  "add_spmat as [] = as" |
-  "add_spmat ((i,a)#as) ((j,b)#bs) = (
-  if i < j then 
-    (i,a) # add_spmat as ((j,b)#bs)
-  else if j < i then
-    (j,b) # add_spmat ((i,a)#as) bs
-  else
-    (i, add_spvec a b) # add_spmat as bs)"
+  "add_spmat [] bs = bs"
+| "add_spmat as [] = as"
+| "add_spmat ((i,a)#as) ((j,b)#bs) = (
+    if i < j then 
+      (i,a) # add_spmat as ((j,b)#bs)
+    else if j < i then
+      (j,b) # add_spmat ((i,a)#as) bs
+    else
+      (i, add_spvec a b) # add_spmat as bs)"
 
 lemma add_spmat_Nil2[simp]: "add_spmat as [] = as"
 by(cases as) auto
@@ -532,28 +537,31 @@
   apply (simp_all add: sorted_spvec_add_spvec)
   done
 
-fun le_spvec :: "('a::lattice_ab_group_add) spvec \<Rightarrow> 'a spvec \<Rightarrow> bool" where
+fun le_spvec :: "('a::lattice_ab_group_add) spvec \<Rightarrow> 'a spvec \<Rightarrow> bool"
+where
 (* "measure (% (a,b). (length a) + (length b))" *)
-  "le_spvec [] [] = True" |
-  "le_spvec ((_,a)#as) [] = (a <= 0 & le_spvec as [])" |
-  "le_spvec [] ((_,b)#bs) = (0 <= b & le_spvec [] bs)" |
-  "le_spvec ((i,a)#as) ((j,b)#bs) = (
-  if (i < j) then a <= 0 & le_spvec as ((j,b)#bs)
-  else if (j < i) then 0 <= b & le_spvec ((i,a)#as) bs
-  else a <= b & le_spvec as bs)"
+  "le_spvec [] [] = True"
+| "le_spvec ((_,a)#as) [] = (a <= 0 & le_spvec as [])"
+| "le_spvec [] ((_,b)#bs) = (0 <= b & le_spvec [] bs)"
+| "le_spvec ((i,a)#as) ((j,b)#bs) = (
+    if (i < j) then a <= 0 & le_spvec as ((j,b)#bs)
+    else if (j < i) then 0 <= b & le_spvec ((i,a)#as) bs
+    else a <= b & le_spvec as bs)"
 
-fun le_spmat :: "('a::lattice_ab_group_add) spmat \<Rightarrow> 'a spmat \<Rightarrow> bool" where
+fun le_spmat :: "('a::lattice_ab_group_add) spmat \<Rightarrow> 'a spmat \<Rightarrow> bool"
+where
 (* "measure (% (a,b). (length a) + (length b))" *)
-  "le_spmat [] [] = True" |
-  "le_spmat ((i,a)#as) [] = (le_spvec a [] & le_spmat as [])" |
-  "le_spmat [] ((j,b)#bs) = (le_spvec [] b & le_spmat [] bs)" |
-  "le_spmat ((i,a)#as) ((j,b)#bs) = (
-  if i < j then (le_spvec a [] & le_spmat as ((j,b)#bs))
-  else if j < i then (le_spvec [] b & le_spmat ((i,a)#as) bs)
-  else (le_spvec a b & le_spmat as bs))"
+  "le_spmat [] [] = True"
+| "le_spmat ((i,a)#as) [] = (le_spvec a [] & le_spmat as [])"
+| "le_spmat [] ((j,b)#bs) = (le_spvec [] b & le_spmat [] bs)"
+| "le_spmat ((i,a)#as) ((j,b)#bs) = (
+    if i < j then (le_spvec a [] & le_spmat as ((j,b)#bs))
+    else if j < i then (le_spvec [] b & le_spmat ((i,a)#as) bs)
+    else (le_spvec a b & le_spmat as bs))"
 
 definition disj_matrices :: "('a::zero) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool" where
-  "disj_matrices A B == (! j i. (Rep_matrix A j i \<noteq> 0) \<longrightarrow> (Rep_matrix B j i = 0)) & (! j i. (Rep_matrix B j i \<noteq> 0) \<longrightarrow> (Rep_matrix A j i = 0))"  
+  "disj_matrices A B \<longleftrightarrow>
+    (! j i. (Rep_matrix A j i \<noteq> 0) \<longrightarrow> (Rep_matrix B j i = 0)) & (! j i. (Rep_matrix B j i \<noteq> 0) \<longrightarrow> (Rep_matrix A j i = 0))"  
 
 declare [[simp_depth_limit = 6]]
 
@@ -730,13 +738,15 @@
 
 declare [[simp_depth_limit = 999]]
 
-primrec abs_spmat :: "('a::lattice_ring) spmat \<Rightarrow> 'a spmat" where
-  "abs_spmat [] = []" |
-  "abs_spmat (a#as) = (fst a, abs_spvec (snd a))#(abs_spmat as)"
+primrec abs_spmat :: "('a::lattice_ring) spmat \<Rightarrow> 'a spmat"
+where
+  "abs_spmat [] = []"
+| "abs_spmat (a#as) = (fst a, abs_spvec (snd a))#(abs_spmat as)"
 
-primrec minus_spmat :: "('a::lattice_ring) spmat \<Rightarrow> 'a spmat" where
-  "minus_spmat [] = []" |
-  "minus_spmat (a#as) = (fst a, minus_spvec (snd a))#(minus_spmat as)"
+primrec minus_spmat :: "('a::lattice_ring) spmat \<Rightarrow> 'a spmat"
+where
+  "minus_spmat [] = []"
+| "minus_spmat (a#as) = (fst a, minus_spvec (snd a))#(minus_spmat as)"
 
 lemma sparse_row_matrix_minus:
   "sparse_row_matrix (minus_spmat A) = - (sparse_row_matrix A)"
@@ -801,8 +811,8 @@
   apply (simp_all add: sorted_spvec_abs_spvec)
   done
 
-definition diff_spmat :: "('a::lattice_ring) spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat" where
-  "diff_spmat A B == add_spmat A (minus_spmat B)"
+definition diff_spmat :: "('a::lattice_ring) spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat"
+  where "diff_spmat A B = add_spmat A (minus_spmat B)"
 
 lemma sorted_spmat_diff_spmat: "sorted_spmat A \<Longrightarrow> sorted_spmat B \<Longrightarrow> sorted_spmat (diff_spmat A B)"
   by (simp add: diff_spmat_def sorted_spmat_minus_spmat sorted_spmat_add_spmat)
@@ -813,8 +823,8 @@
 lemma sparse_row_diff_spmat: "sparse_row_matrix (diff_spmat A B ) = (sparse_row_matrix A) - (sparse_row_matrix B)"
   by (simp add: diff_spmat_def sparse_row_add_spmat sparse_row_matrix_minus)
 
-definition sorted_sparse_matrix :: "'a spmat \<Rightarrow> bool" where
-  "sorted_sparse_matrix A == (sorted_spvec A) & (sorted_spmat A)"
+definition sorted_sparse_matrix :: "'a spmat \<Rightarrow> bool"
+  where "sorted_sparse_matrix A \<longleftrightarrow> sorted_spvec A & sorted_spmat A"
 
 lemma sorted_sparse_matrix_imp_spvec: "sorted_sparse_matrix A \<Longrightarrow> sorted_spvec A"
   by (simp add: sorted_sparse_matrix_def)
@@ -841,29 +851,25 @@
 
 lemma if_case_eq: "(if b then x else y) = (case b of True => x | False => y)" by simp
 
-consts
-  pprt_spvec :: "('a::{lattice_ab_group_add}) spvec \<Rightarrow> 'a spvec"
-  nprt_spvec :: "('a::{lattice_ab_group_add}) spvec \<Rightarrow> 'a spvec"
-  pprt_spmat :: "('a::{lattice_ab_group_add}) spmat \<Rightarrow> 'a spmat"
-  nprt_spmat :: "('a::{lattice_ab_group_add}) spmat \<Rightarrow> 'a spmat"
+primrec pprt_spvec :: "('a::{lattice_ab_group_add}) spvec \<Rightarrow> 'a spvec"
+where
+  "pprt_spvec [] = []"
+| "pprt_spvec (a#as) = (fst a, pprt (snd a)) # (pprt_spvec as)"
 
-primrec
-  "pprt_spvec [] = []"
-  "pprt_spvec (a#as) = (fst a, pprt (snd a)) # (pprt_spvec as)"
-
-primrec
+primrec nprt_spvec :: "('a::{lattice_ab_group_add}) spvec \<Rightarrow> 'a spvec"
+where
   "nprt_spvec [] = []"
-  "nprt_spvec (a#as) = (fst a, nprt (snd a)) # (nprt_spvec as)"
+| "nprt_spvec (a#as) = (fst a, nprt (snd a)) # (nprt_spvec as)"
 
-primrec 
+primrec pprt_spmat :: "('a::{lattice_ab_group_add}) spmat \<Rightarrow> 'a spmat"
+where
   "pprt_spmat [] = []"
-  "pprt_spmat (a#as) = (fst a, pprt_spvec (snd a))#(pprt_spmat as)"
-  (*case (pprt_spvec (snd a)) of [] \<Rightarrow> (pprt_spmat as) | y#ys \<Rightarrow> (fst a, y#ys)#(pprt_spmat as))"*)
+| "pprt_spmat (a#as) = (fst a, pprt_spvec (snd a))#(pprt_spmat as)"
 
-primrec 
+primrec nprt_spmat :: "('a::{lattice_ab_group_add}) spmat \<Rightarrow> 'a spmat"
+where
   "nprt_spmat [] = []"
-  "nprt_spmat (a#as) = (fst a, nprt_spvec (snd a))#(nprt_spmat as)"
-  (*case (nprt_spvec (snd a)) of [] \<Rightarrow> (nprt_spmat as) | y#ys \<Rightarrow> (fst a, y#ys)#(nprt_spmat as))"*)
+| "nprt_spmat (a#as) = (fst a, nprt_spvec (snd a))#(nprt_spmat as)"
 
 
 lemma pprt_add: "disj_matrices A (B::(_::lattice_ring) matrix) \<Longrightarrow> pprt (A+B) = pprt A + pprt B"
@@ -1012,7 +1018,7 @@
   done
 
 definition mult_est_spmat :: "('a::lattice_ring) spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat" where
-  "mult_est_spmat r1 r2 s1 s2 == 
+  "mult_est_spmat r1 r2 s1 s2 =
   add_spmat (mult_spmat (pprt_spmat s2) (pprt_spmat r2)) (add_spmat (mult_spmat (pprt_spmat s1) (nprt_spmat r2)) 
   (add_spmat (mult_spmat (nprt_spmat s2) (pprt_spmat r1)) (mult_spmat (nprt_spmat s1) (nprt_spmat r1))))"  
 
diff -r 6daf896bca5e -r 01d2ef471ffe src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Wed Aug 11 12:04:06 2010 +0200
+++ b/src/HOL/Tools/record.ML	Wed Aug 11 12:50:33 2010 +0200
@@ -74,7 +74,7 @@
 
 val tuple_iso_tuple = (@{const_name Record.tuple_iso_tuple}, @{thm tuple_iso_tuple});
 
-fun named_cterm_instantiate values thm =
+fun named_cterm_instantiate values thm =  (* FIXME eliminate *)
   let
     fun match name ((name', _), _) = name = name';
     fun getvar name =
diff -r 6daf896bca5e -r 01d2ef471ffe src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Wed Aug 11 12:04:06 2010 +0200
+++ b/src/Pure/General/markup.scala	Wed Aug 11 12:50:33 2010 +0200
@@ -203,6 +203,7 @@
   val ERROR = "error"
   val DEBUG = "debug"
   val SYSTEM = "system"
+  val INPUT = "input"
   val STDIN = "stdin"
   val STDOUT = "stdout"
   val SIGNAL = "signal"
diff -r 6daf896bca5e -r 01d2ef471ffe src/Pure/General/source.ML
--- a/src/Pure/General/source.ML	Wed Aug 11 12:04:06 2010 +0200
+++ b/src/Pure/General/source.ML	Wed Aug 11 12:50:33 2010 +0200
@@ -19,7 +19,7 @@
   val exhausted: ('a, 'b) source -> ('a, 'a list) source
   val of_string: string -> (string, string list) source
   val of_string_limited: int -> string -> (string, substring) source
-  val tty: (string, unit) source
+  val tty: TextIO.instream -> (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 ->
     ('b, 'e) source -> ('c, 'a * ('b, 'e) source) source
@@ -129,11 +129,11 @@
       | SOME _ => TextIO.input instream :: slurp ());
   in maps explode (slurp ()) end;
 
-val tty = make_source [] () default_prompt (fn prompt => fn () =>
-  let val input = slurp_input TextIO.stdIn in
+fun tty in_stream = make_source [] () default_prompt (fn prompt => fn () =>
+  let val input = slurp_input in_stream in
     if exists (fn c => c = "\n") input then (input, ())
     else
-      (case (Output.prompt prompt; TextIO.inputLine TextIO.stdIn) of
+      (case (Output.prompt prompt; TextIO.inputLine in_stream) of
         SOME line => (input @ explode line, ())
       | NONE => (input, ()))
   end);
diff -r 6daf896bca5e -r 01d2ef471ffe src/Pure/General/xml.ML
--- a/src/Pure/General/xml.ML	Wed Aug 11 12:04:06 2010 +0200
+++ b/src/Pure/General/xml.ML	Wed Aug 11 12:50:33 2010 +0200
@@ -10,6 +10,7 @@
   datatype tree =
       Elem of Markup.T * tree list
     | Text of string
+  type body = tree list
   val add_content: tree -> Buffer.T -> Buffer.T
   val header: string
   val text: string -> string
@@ -35,6 +36,8 @@
     Elem of Markup.T * tree list
   | Text of string;
 
+type body = tree list;
+
 fun add_content (Elem (_, ts)) = fold add_content ts
   | add_content (Text s) = Buffer.add s;
 
diff -r 6daf896bca5e -r 01d2ef471ffe src/Pure/General/xml.scala
--- a/src/Pure/General/xml.scala	Wed Aug 11 12:04:06 2010 +0200
+++ b/src/Pure/General/xml.scala	Wed Aug 11 12:50:33 2010 +0200
@@ -17,54 +17,52 @@
 
   type Attributes = List[(String, String)]
 
-  sealed abstract class Tree {
-    override def toString = {
-      val s = new StringBuilder
-      append_tree(this, s)
-      s.toString
-    }
-  }
+  sealed abstract class Tree { override def toString = string_of_tree(this) }
   case class Elem(markup: Markup, body: List[Tree]) extends Tree
   case class Text(content: String) extends Tree
 
   def elem(name: String, body: List[Tree]) = Elem(Markup(name, Nil), body)
   def elem(name: String) = Elem(Markup(name, Nil), Nil)
 
+  type Body = List[Tree]
+
 
   /* string representation */
 
-  private def append_text(text: String, s: StringBuilder) {
-    if (text == null) s ++= text
-    else {
-      for (c <- text.iterator) c match {
-        case '<' => s ++= "&lt;"
-        case '>' => s ++= "&gt;"
-        case '&' => s ++= "&amp;"
-        case '"' => s ++= "&quot;"
-        case '\'' => s ++= "&apos;"
-        case _ => s += c
+  def string_of_body(body: Body): String =
+  {
+    val s = new StringBuilder
+
+    def text(txt: String) {
+      if (txt == null) s ++= txt
+      else {
+        for (c <- txt.iterator) c match {
+          case '<' => s ++= "&lt;"
+          case '>' => s ++= "&gt;"
+          case '&' => s ++= "&amp;"
+          case '"' => s ++= "&quot;"
+          case '\'' => s ++= "&apos;"
+          case _ => s += c
+        }
       }
     }
+    def attrib(p: (String, String)) { s ++= " "; s ++= p._1; s ++= "=\""; text(p._2); s ++= "\"" }
+    def elem(markup: Markup) { s ++= markup.name; markup.properties.foreach(attrib) }
+    def tree(t: Tree): Unit =
+      t match {
+        case Elem(markup, Nil) =>
+          s ++= "<"; elem(markup); s ++= "/>"
+        case Elem(markup, ts) =>
+          s ++= "<"; elem(markup); s ++= ">"
+          ts.foreach(tree)
+          s ++= "</"; s ++= markup.name; s ++= ">"
+        case Text(txt) => text(txt)
+      }
+    body.foreach(tree)
+    s.toString
   }
 
-  private def append_elem(name: String, atts: Attributes, s: StringBuilder) {
-    s ++= name
-    for ((a, x) <- atts) {
-      s ++= " "; s ++= a; s ++= "=\""; append_text(x, s); s ++= "\""
-    }
-  }
-
-  private def append_tree(tree: Tree, s: StringBuilder) {
-    tree match {
-      case Elem(Markup(name, atts), Nil) =>
-        s ++= "<"; append_elem(name, atts, s); s ++= "/>"
-      case Elem(Markup(name, atts), ts) =>
-        s ++= "<"; append_elem(name, atts, s); s ++= ">"
-        for (t <- ts) append_tree(t, s)
-        s ++= "</"; s ++= name; s ++= ">"
-      case Text(text) => append_text(text, s)
-    }
-  }
+  def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
 
 
   /* iterate over content */
diff -r 6daf896bca5e -r 01d2ef471ffe src/Pure/General/xml_data.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/xml_data.ML	Wed Aug 11 12:50:33 2010 +0200
@@ -0,0 +1,128 @@
+(*  Title:      Pure/General/xml_data.ML
+    Author:     Makarius
+
+XML as basic data representation language.
+*)
+
+signature XML_DATA =
+sig
+  exception XML_ATOM of string
+  exception XML_BODY of XML.body
+  val make_properties: Properties.T -> XML.body
+  val dest_properties: XML.body -> Properties.T
+  val make_string: string -> XML.body
+  val dest_string : XML.body -> string
+  val make_int: int -> XML.body
+  val dest_int : XML.body -> int
+  val make_bool: bool -> XML.body
+  val dest_bool: XML.body -> bool
+  val make_unit: unit -> XML.body
+  val dest_unit: XML.body -> unit
+  val make_pair: ('a -> XML.body) -> ('b -> XML.body) -> 'a * 'b -> XML.body
+  val dest_pair: (XML.body -> 'a) -> (XML.body -> 'b) -> XML.body -> 'a * 'b
+  val make_triple:
+    ('a -> XML.body) -> ('b -> XML.body) -> ('c -> XML.body) -> 'a * 'b * 'c -> XML.body
+  val dest_triple:
+    (XML.body -> 'a) -> (XML.body -> 'b) -> (XML.body -> 'c) -> XML.body -> 'a * 'b * 'c
+  val make_list: ('a -> XML.body) -> 'a list -> XML.body
+  val dest_list: (XML.body -> 'a) -> XML.body -> 'a list
+  val make_option: ('a -> XML.body) -> 'a option -> XML.body
+  val dest_option: (XML.body -> 'a) -> XML.body -> 'a option
+end;
+
+structure XML_Data: XML_DATA =
+struct
+
+(* basic values *)
+
+exception XML_ATOM of string;
+
+
+fun make_int_atom i = signed_string_of_int i;
+
+fun dest_int_atom s =
+  (case Int.fromString s of
+    SOME i => i
+  | NONE => raise XML_ATOM s);
+
+
+fun make_bool_atom false = "0"
+  | make_bool_atom true = "1";
+
+fun dest_bool_atom "0" = false
+  | dest_bool_atom "1" = true
+  | dest_bool_atom s = raise XML_ATOM s;
+
+
+fun make_unit_atom () = "";
+
+fun dest_unit_atom "" = ()
+  | dest_unit_atom s = raise XML_ATOM s;
+
+
+(* structural nodes *)
+
+exception XML_BODY of XML.tree list;
+
+fun make_node ts = XML.Elem ((":", []), ts);
+
+fun dest_node (XML.Elem ((":", []), ts)) = ts
+  | dest_node t = raise XML_BODY [t];
+
+
+(* representation of standard types *)
+
+fun make_properties props = [XML.Elem ((":", props), [])];
+
+fun dest_properties [XML.Elem ((":", props), [])] = props
+  | dest_properties ts = raise XML_BODY ts;
+
+
+fun make_string "" = []
+  | make_string s = [XML.Text s];
+
+fun dest_string [] = ""
+  | dest_string [XML.Text s] = s
+  | dest_string ts = raise XML_BODY ts;
+
+
+val make_int = make_string o make_int_atom;
+val dest_int = dest_int_atom o dest_string;
+
+val make_bool = make_string o make_bool_atom;
+val dest_bool = dest_bool_atom o dest_string;
+
+val make_unit = make_string o make_unit_atom;
+val dest_unit = dest_unit_atom o dest_string;
+
+
+fun make_pair make1 make2 (x, y) = [make_node (make1 x), make_node (make2 y)];
+
+fun dest_pair dest1 dest2 [t1, t2] = (dest1 (dest_node t1), dest2 (dest_node t2))
+  | dest_pair _ _ ts = raise XML_BODY ts;
+
+
+fun make_triple make1 make2 make3 (x, y, z) =
+  [make_node (make1 x), make_node (make2 y), make_node (make3 z)];
+
+fun dest_triple dest1 dest2 dest3 [t1, t2, t3] =
+      (dest1 (dest_node t1), dest2 (dest_node t2), dest3 (dest_node t3))
+  | dest_triple _ _ _ ts = raise XML_BODY ts;
+
+
+fun make_list make xs = map (make_node o make) xs;
+
+fun dest_list dest ts = map (dest o dest_node) ts;
+
+
+fun make_option make NONE = make_list make []
+  | make_option make (SOME x) = make_list make [x];
+
+fun dest_option dest ts =
+  (case dest_list dest ts of
+    [] => NONE
+  | [x] => SOME x
+  | _ => raise XML_BODY ts);
+
+end;
+
diff -r 6daf896bca5e -r 01d2ef471ffe src/Pure/General/xml_data.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/xml_data.scala	Wed Aug 11 12:50:33 2010 +0200
@@ -0,0 +1,125 @@
+/*  Title:      Pure/General/xml_data.scala
+    Author:     Makarius
+
+XML as basic data representation language.
+*/
+
+package isabelle
+
+
+
+object XML_Data
+{
+  /* basic values */
+
+  class XML_Atom(s: String) extends Exception(s)
+
+
+  private def make_int_atom(i: Int): String = i.toString
+
+  private def dest_int_atom(s: String): Int =
+    try { Integer.parseInt(s) }
+    catch { case e: NumberFormatException => throw new XML_Atom(s) }
+
+
+  private def make_bool_atom(b: Boolean): String = if (b) "1" else "0"
+
+  private def dest_bool_atom(s: String): Boolean =
+    if (s == "1") true
+    else if (s == "0") false
+    else throw new XML_Atom(s)
+
+
+  private def make_unit_atom(u: Unit) = ""
+
+  private def dest_unit_atom(s: String): Unit =
+    if (s == "") () else throw new XML_Atom(s)
+
+
+  /* structural nodes */
+
+  class XML_Body(body: XML.Body) extends Exception
+
+  private def make_node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
+
+  private def dest_node(t: XML.Tree): XML.Body =
+    t match {
+      case XML.Elem(Markup(":", Nil), ts) => ts
+      case _ => throw new XML_Body(List(t))
+    }
+
+
+  /* representation of standard types */
+
+  def make_properties(props: List[(String, String)]): XML.Body =
+    List(XML.Elem(Markup(":", props), Nil))
+
+  def dest_properties(ts: XML.Body): List[(String, String)] =
+    ts match {
+      case List(XML.Elem(Markup(":", props), Nil)) => props
+      case _ => throw new XML_Body(ts)
+    }
+
+
+  def make_string(s: String): XML.Body = if (s.isEmpty) Nil else List(XML.Text(s))
+
+  def dest_string(ts: XML.Body): String =
+    ts match {
+      case Nil => ""
+      case List(XML.Text(s)) => s
+      case _ => throw new XML_Body(ts)
+    }
+
+
+  def make_int(i: Int): XML.Body = make_string(make_int_atom(i))
+  def dest_int(ts: XML.Body): Int = dest_int_atom(dest_string(ts))
+
+  def make_bool(b: Boolean): XML.Body = make_string(make_bool_atom(b))
+  def dest_bool(ts: XML.Body) = dest_bool_atom(dest_string(ts))
+
+  def make_unit(u: Unit): XML.Body = make_string(make_unit_atom(u))
+  def dest_unit(ts: XML.Body): Unit = dest_unit_atom(dest_string(ts))
+
+
+  def make_pair[A, B](make1: A => XML.Body)(make2: B => XML.Body)(p: (A, B)): XML.Body =
+    List(make_node(make1(p._1)), make_node(make2(p._2)))
+
+  def dest_pair[A, B](dest1: XML.Body => A)(dest2: XML.Body => B)(ts: XML.Body): (A, B) =
+    ts match {
+      case List(t1, t2) => (dest1(dest_node(t1)), dest2(dest_node(t2)))
+      case _ => throw new XML_Body(ts)
+    }
+
+
+  def make_triple[A, B, C](make1: A => XML.Body)(make2: B => XML.Body)(make3: C => XML.Body)
+      (p: (A, B, C)): XML.Body =
+    List(make_node(make1(p._1)), make_node(make2(p._2)), make_node(make3(p._3)))
+
+  def dest_triple[A, B, C](dest1: XML.Body => A)(dest2: XML.Body => B)(dest3: XML.Body => C)
+      (ts: XML.Body): (A, B, C) =
+    ts match {
+      case List(t1, t2, t3) => (dest1(dest_node(t1)), dest2(dest_node(t2)), dest3(dest_node(t3)))
+      case _ => throw new XML_Body(ts)
+    }
+
+
+  def make_list[A](make: A => XML.Body)(xs: List[A]): XML.Body =
+    xs.map((x: A) => make_node(make(x)))
+
+  def dest_list[A](dest: XML.Body => A)(ts: XML.Body): List[A] =
+    ts.map((t: XML.Tree) => dest(dest_node(t)))
+
+
+  def make_option[A](make: A => XML.Body)(opt: Option[A]): XML.Body =
+    opt match {
+      case None => make_list(make)(Nil)
+      case Some(x) => make_list(make)(List(x))
+    }
+
+  def dest_option[A](dest: XML.Body => A)(ts: XML.Body): Option[A] =
+    dest_list(dest)(ts) match {
+      case Nil => None
+      case List(x) => Some(x)
+      case _ => throw new XML_Body(ts)
+    }
+}
diff -r 6daf896bca5e -r 01d2ef471ffe src/Pure/General/yxml.ML
--- a/src/Pure/General/yxml.ML	Wed Aug 11 12:04:06 2010 +0200
+++ b/src/Pure/General/yxml.ML	Wed Aug 11 12:50:33 2010 +0200
@@ -15,11 +15,11 @@
 
 signature YXML =
 sig
-  val binary_text: string -> string
+  val escape_controls: string -> string
   val output_markup: Markup.T -> string * string
   val element: string -> XML.attributes -> string list -> string
   val string_of: XML.tree -> string
-  val parse_body: string -> XML.tree list
+  val parse_body: string -> XML.body
   val parse: string -> XML.tree
 end;
 
@@ -28,14 +28,14 @@
 
 (** string representation **)
 
-(* binary_text -- idempotent recoding *)
+(* idempotent recoding of certain low ASCII control characters *)
 
 fun pseudo_utf8 c =
   if Symbol.is_ascii_control c
   then chr 192 ^ chr (128 + ord c)
   else c;
 
-fun binary_text str =
+fun escape_controls str =
   if exists_string Symbol.is_ascii_control str
   then translate_string pseudo_utf8 str
   else str;
diff -r 6daf896bca5e -r 01d2ef471ffe src/Pure/General/yxml.scala
--- a/src/Pure/General/yxml.scala	Wed Aug 11 12:04:06 2010 +0200
+++ b/src/Pure/General/yxml.scala	Wed Aug 11 12:50:33 2010 +0200
@@ -20,6 +20,27 @@
   private val Y_string = Y.toString
 
 
+  /* string representation */  // FIXME byte array version with pseudo-utf-8 (!?)
+
+  def string_of_body(body: XML.Body): String =
+  {
+    val s = new StringBuilder
+    def attrib(p: (String, String)) { s += Y; s ++= p._1; s += '='; s ++= p._2 }
+    def tree(t: XML.Tree): Unit =
+      t match {
+        case XML.Elem(Markup(name, atts), ts) =>
+          s += X; s += Y; s++= name; atts.foreach(attrib); s += X
+          ts.foreach(tree)
+          s += X; s += Y; s += X
+        case XML.Text(text) => s ++= text
+      }
+    body.foreach(tree)
+    s.toString
+  }
+
+  def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
+
+
   /* decoding pseudo UTF-8 */
 
   private class Decode_Chars(decode: String => String,
@@ -59,7 +80,7 @@
   }
 
 
-  def parse_body(source: CharSequence): List[XML.Tree] =
+  def parse_body(source: CharSequence): XML.Body =
   {
     /* stack operations */
 
@@ -120,7 +141,7 @@
     XML.elem (Markup.MALFORMED,
       List(XML.Text(source.toString.replace(X_string, "\\<^X>").replace(Y_string, "\\<^Y>"))))
 
-  def parse_body_failsafe(source: CharSequence): List[XML.Tree] =
+  def parse_body_failsafe(source: CharSequence): XML.Body =
   {
     try { parse_body(source) }
     catch { case _: RuntimeException => List(markup_failsafe(source)) }
diff -r 6daf896bca5e -r 01d2ef471ffe src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Wed Aug 11 12:04:06 2010 +0200
+++ b/src/Pure/IsaMakefile	Wed Aug 11 12:50:33 2010 +0200
@@ -59,13 +59,14 @@
   General/sha1_polyml.ML General/secure.ML General/seq.ML		\
   General/source.ML General/stack.ML General/symbol.ML			\
   General/symbol_pos.ML General/table.ML General/url.ML General/xml.ML	\
-  General/yxml.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML		\
-  Isar/calculation.ML Isar/class.ML Isar/class_target.ML Isar/code.ML	\
-  Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML		\
-  Isar/expression.ML Isar/generic_target.ML Isar/isar_cmd.ML		\
-  Isar/isar_document.ML	Isar/isar_syn.ML Isar/keyword.ML		\
-  Isar/local_defs.ML Isar/local_syntax.ML Isar/local_theory.ML		\
-  Isar/locale.ML Isar/method.ML Isar/object_logic.ML Isar/obtain.ML	\
+  General/xml_data.ML General/yxml.ML Isar/args.ML Isar/attrib.ML	\
+  Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML			\
+  Isar/class_target.ML Isar/code.ML Isar/constdefs.ML			\
+  Isar/context_rules.ML Isar/element.ML Isar/expression.ML		\
+  Isar/generic_target.ML Isar/isar_cmd.ML Isar/isar_document.ML		\
+  Isar/isar_syn.ML Isar/keyword.ML Isar/local_defs.ML			\
+  Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML		\
+  Isar/method.ML Isar/object_logic.ML Isar/obtain.ML			\
   Isar/outer_syntax.ML Isar/overloading.ML Isar/parse.ML		\
   Isar/parse_spec.ML Isar/parse_value.ML Isar/proof.ML			\
   Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML	\
@@ -83,7 +84,31 @@
   ProofGeneral/pgip_markup.ML ProofGeneral/pgip_output.ML		\
   ProofGeneral/pgip_parser.ML ProofGeneral/pgip_tests.ML		\
   ProofGeneral/pgip_types.ML ProofGeneral/preferences.ML		\
-  ProofGeneral/proof_general_emacs.ML					\
+  ProofGeneral/proof_general_emacs.ML General/yxml.ML Isar/args.ML	\
+  Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML	\
+  Isar/class_target.ML Isar/code.ML Isar/constdefs.ML			\
+  Isar/context_rules.ML Isar/element.ML Isar/expression.ML		\
+  Isar/isar_cmd.ML Isar/isar_document.ML Isar/isar_syn.ML		\
+  Isar/keyword.ML Isar/local_defs.ML Isar/local_syntax.ML		\
+  Isar/local_theory.ML Isar/locale.ML Isar/method.ML			\
+  Isar/object_logic.ML Isar/obtain.ML Isar/outer_syntax.ML		\
+  Isar/overloading.ML Isar/parse.ML Isar/parse_spec.ML			\
+  Isar/parse_value.ML Isar/proof.ML Isar/proof_context.ML		\
+  Isar/proof_display.ML Isar/proof_node.ML Isar/rule_cases.ML		\
+  Isar/rule_insts.ML Isar/runtime.ML Isar/skip_proof.ML			\
+  Isar/spec_rules.ML Isar/specification.ML Isar/theory_target.ML	\
+  Isar/token.ML Isar/toplevel.ML Isar/typedecl.ML ML/ml_antiquote.ML	\
+  ML/ml_compiler.ML ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML	\
+  ML/ml_env.ML ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML		\
+  ML/ml_thms.ML ML-Systems/install_pp_polyml.ML				\
+  ML-Systems/install_pp_polyml-5.3.ML ML-Systems/use_context.ML		\
+  Proof/extraction.ML PIDE/document.ML Proof/proof_rewrite_rules.ML	\
+  Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML	\
+  ProofGeneral/pgip.ML ProofGeneral/pgip_input.ML			\
+  ProofGeneral/pgip_isabelle.ML ProofGeneral/pgip_markup.ML		\
+  ProofGeneral/pgip_output.ML ProofGeneral/pgip_parser.ML		\
+  ProofGeneral/pgip_tests.ML ProofGeneral/pgip_types.ML			\
+  ProofGeneral/preferences.ML ProofGeneral/proof_general_emacs.ML	\
   ProofGeneral/proof_general_pgip.ML Pure.thy ROOT.ML Syntax/ast.ML	\
   Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML			\
   Syntax/printer.ML Syntax/simple_syntax.ML Syntax/syn_ext.ML		\
diff -r 6daf896bca5e -r 01d2ef471ffe src/Pure/Isar/isar_document.ML
--- a/src/Pure/Isar/isar_document.ML	Wed Aug 11 12:04:06 2010 +0200
+++ b/src/Pure/Isar/isar_document.ML	Wed Aug 11 12:50:33 2010 +0200
@@ -143,10 +143,16 @@
 
 in
 
-fun define_command (id: Document.command_id) tr =
-  NAMED_CRITICAL "Isar" (fn () =>
-    Unsynchronized.change global_commands (Symtab.update_new (id, Toplevel.put_id id tr))
-      handle Symtab.DUP dup => err_dup "command" dup);
+fun define_command (id: Document.command_id) text =
+  let
+    val tr =
+      Position.setmp_thread_data (Position.id_only id) (fn () =>
+        Outer_Syntax.prepare_command (Position.id id) text) ();
+  in
+    NAMED_CRITICAL "Isar" (fn () =>
+      Unsynchronized.change global_commands (Symtab.update_new (id, Toplevel.put_id id tr))
+        handle Symtab.DUP dup => err_dup "command" dup)
+  end;
 
 fun the_command (id: Document.command_id) =
   (case Symtab.lookup (! global_commands) id of
@@ -178,7 +184,7 @@
 
 
 
-(** main operations **)
+(** document editing **)
 
 (* execution *)
 
@@ -241,52 +247,50 @@
 in
 
 fun edit_document (old_id: Document.version_id) (new_id: Document.version_id) edits =
-  NAMED_CRITICAL "Isar" (fn () =>
-    let
-      val old_document = the_document old_id;
-      val new_document = fold edit_nodes edits old_document;
+  Position.setmp_thread_data (Position.id_only new_id) (fn () =>
+    NAMED_CRITICAL "Isar" (fn () =>
+      let
+        val old_document = the_document old_id;
+        val new_document = fold edit_nodes edits old_document;
 
-      fun update_node name node =
-        (case first_entry (is_changed (the_node old_document name)) node of
-          NONE => ([], node)
-        | SOME (prev, id, _) =>
-            let
-              val prev_state_id = the (#state (the_entry node (the prev)));
-              val (_, updates) = fold_entries id (new_state name o #1) node (prev_state_id, []);
-              val node' = fold set_entry_state updates node;
-            in (rev updates, node') end);
+        fun update_node name node =
+          (case first_entry (is_changed (the_node old_document name)) node of
+            NONE => ([], node)
+          | SOME (prev, id, _) =>
+              let
+                val prev_state_id = the (#state (the_entry node (the prev)));
+                val (_, updates) = fold_entries id (new_state name o #1) node (prev_state_id, []);
+                val node' = fold set_entry_state updates node;
+              in (rev updates, node') end);
 
-      (* FIXME proper node deps *)
-      val (updatess, new_document') =
-        (Graph.keys new_document, new_document)
-          |-> fold_map (fn name => Graph.map_node_yield name (update_node name));
+        (* FIXME proper node deps *)
+        val (updatess, new_document') =
+          (Graph.keys new_document, new_document)
+            |-> fold_map (fn name => Graph.map_node_yield name (update_node name));
 
-      val _ = define_document new_id new_document';
-      val _ = updates_status (flat updatess);
-      val _ = execute new_document';
-    in () end);
+        val _ = define_document new_id new_document';
+        val _ = updates_status (flat updatess);
+        val _ = execute new_document';
+      in () end)) ();
 
 end;
 
 
 
-(** concrete syntax **)
+(** Isabelle process commands **)
+
+val _ =
+  Isabelle_Process.add_command "Isar_Document.define_command"
+    (fn [id, text] => define_command id text);
 
 val _ =
-  Outer_Syntax.internal_command "Isar.define_command"
-    (Parse.string -- Parse.string >> (fn (id, text) =>
-      Toplevel.position (Position.id_only id) o
-      Toplevel.imperative (fn () =>
-        define_command id (Outer_Syntax.prepare_command (Position.id id) text))));
-
-val _ =
-  Outer_Syntax.internal_command "Isar.edit_document"
-    (Parse.string -- Parse.string --
-      Parse_Value.list
-        (Parse.string -- Scan.option (Parse_Value.list (Parse.string -- Scan.option Parse.string)))
-      >> (fn ((old_id, new_id), edits) =>
-          Toplevel.position (Position.id_only new_id) o
-          Toplevel.imperative (fn () => edit_document old_id new_id edits)));
+  Isabelle_Process.add_command "Isar_Document.edit_document"
+    (fn [old_id, new_id, edits] =>
+      edit_document old_id new_id
+        (XML_Data.dest_list (XML_Data.dest_pair XML_Data.dest_string
+            (XML_Data.dest_option (XML_Data.dest_list
+                (XML_Data.dest_pair XML_Data.dest_string
+                  (XML_Data.dest_option XML_Data.dest_string))))) (YXML.parse_body edits)));
 
 end;
 
diff -r 6daf896bca5e -r 01d2ef471ffe src/Pure/Isar/isar_document.scala
--- a/src/Pure/Isar/isar_document.scala	Wed Aug 11 12:04:06 2010 +0200
+++ b/src/Pure/Isar/isar_document.scala	Wed Aug 11 12:50:33 2010 +0200
@@ -37,10 +37,8 @@
 
   /* commands */
 
-  def define_command(id: Document.Command_ID, text: String) {
-    output_sync("Isar.define_command " + Isabelle_Syntax.encode_string(id) + " " +
-      Isabelle_Syntax.encode_string(text))
-  }
+  def define_command(id: Document.Command_ID, text: String): Unit =
+    input("Isar_Document.define_command", id, text)
 
 
   /* documents */
@@ -48,38 +46,14 @@
   def edit_document(old_id: Document.Version_ID, new_id: Document.Version_ID,
       edits: List[Document.Edit[Document.Command_ID]])
   {
-    def append_edit(
-        edit: (Option[Document.Command_ID], Option[Document.Command_ID]), result: StringBuilder)
-    {
-      Isabelle_Syntax.append_string(edit._1 getOrElse Document.NO_ID, result)
-      edit._2 match {
-        case None =>
-        case Some(id2) =>
-          result.append(" ")
-          Isabelle_Syntax.append_string(id2, result)
-      }
-    }
+    def make_id1(id1: Option[Document.Command_ID]): XML.Body =
+      XML_Data.make_string(id1 getOrElse Document.NO_ID)
+    val arg =
+      XML_Data.make_list(
+        XML_Data.make_pair(XML_Data.make_string)(
+          XML_Data.make_option(XML_Data.make_list(
+              XML_Data.make_pair(make_id1)(XML_Data.make_option(XML_Data.make_string))))))(edits)
 
-    def append_node_edit(
-        edit: (String, Option[List[(Option[Document.Command_ID], Option[Document.Command_ID])]]),
-        result: StringBuilder)
-    {
-      Isabelle_Syntax.append_string(edit._1, result)
-      edit._2 match {
-        case None =>
-        case Some(eds) =>
-          result.append(" ")
-          Isabelle_Syntax.append_list(append_edit, eds, result)
-      }
-    }
-
-    val buf = new StringBuilder(40)
-    buf.append("Isar.edit_document ")
-    Isabelle_Syntax.append_string(old_id, buf)
-    buf.append(" ")
-    Isabelle_Syntax.append_string(new_id, buf)
-    buf.append(" ")
-    Isabelle_Syntax.append_list(append_node_edit, edits, buf)
-    output_sync(buf.toString)
+    input("Isar_Document.edit_document", old_id, new_id, YXML.string_of_body(arg))
   }
 }
diff -r 6daf896bca5e -r 01d2ef471ffe src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Wed Aug 11 12:04:06 2010 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Wed Aug 11 12:50:33 2010 +0200
@@ -29,7 +29,7 @@
   val parse: Position.T -> string -> Toplevel.transition list
   val process_file: Path.T -> theory -> theory
   type isar
-  val isar: bool -> isar
+  val isar: TextIO.instream -> bool -> isar
   val prepare_command: Position.T -> string -> Toplevel.transition
   val load_thy: string -> (unit -> theory) -> Position.T -> string -> (unit -> unit) * theory
 end;
@@ -222,8 +222,8 @@
   Source.source) Source.source) Source.source) Source.source)
   Source.source) Source.source) Source.source) Source.source;
 
-fun isar term : isar =
-  Source.tty
+fun isar in_stream term : isar =
+  Source.tty in_stream
   |> Symbol.source {do_recover = true}
   |> Token.source {do_recover = SOME true} Keyword.get_lexicons Position.none
   |> toplevel_source term (SOME true) get_command;
diff -r 6daf896bca5e -r 01d2ef471ffe src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Wed Aug 11 12:04:06 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Wed Aug 11 12:50:33 2010 +0200
@@ -245,7 +245,8 @@
         sync_thy_loader ();
        Unsynchronized.change print_mode (update (op =) proof_generalN);
        Secure.PG_setup ();
-       Isar.toplevel_loop {init = true, welcome = true, sync = true, secure = Secure.is_secure ()});
+       Isar.toplevel_loop TextIO.stdIn
+        {init = true, welcome = true, sync = true, secure = Secure.is_secure ()});
 
 
 (* fake old ThyLoad -- with new semantics *)
diff -r 6daf896bca5e -r 01d2ef471ffe src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Aug 11 12:04:06 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Aug 11 12:50:33 2010 +0200
@@ -1000,7 +1000,8 @@
 
   val xmlP = XML.parse_comments |-- XML.parse_element >> single
 
-  val tty_src = Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE Source.tty)
+  val tty_src =
+    Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE (Source.tty TextIO.stdIn))
 
   fun pgip_toplevel x = loop true x
 end
diff -r 6daf896bca5e -r 01d2ef471ffe src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Aug 11 12:04:06 2010 +0200
+++ b/src/Pure/ROOT.ML	Wed Aug 11 12:50:33 2010 +0200
@@ -50,6 +50,7 @@
 use "General/buffer.ML";
 use "General/file.ML";
 use "General/xml.ML";
+use "General/xml_data.ML";
 use "General/yxml.ML";
 
 use "General/sha1.ML";
@@ -230,7 +231,7 @@
 use "Isar/proof_node.ML";
 use "Isar/toplevel.ML";
 
-(*theory syntax*)
+(*theory documents*)
 use "Thy/present.ML";
 use "Thy/term_style.ML";
 use "Thy/thy_output.ML";
@@ -239,7 +240,6 @@
 use "old_goals.ML";
 use "Isar/outer_syntax.ML";
 use "Thy/thy_info.ML";
-use "Isar/isar_document.ML";
 
 (*theory and proof operations*)
 use "Isar/rule_insts.ML";
@@ -257,6 +257,7 @@
 use "System/session.ML";
 use "System/isar.ML";
 use "System/isabelle_process.ML";
+use "Isar/isar_document.ML";
 
 
 (* miscellaneous tools and packages for Pure Isabelle *)
diff -r 6daf896bca5e -r 01d2ef471ffe src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Wed Aug 11 12:04:06 2010 +0200
+++ b/src/Pure/System/isabelle_process.ML	Wed Aug 11 12:50:33 2010 +0200
@@ -11,7 +11,10 @@
 signature ISABELLE_PROCESS =
 sig
   val isabelle_processN: string
-  val init: string -> unit
+  val add_command: string -> (string list -> unit) -> unit
+  val command: string -> string list -> unit
+  val crashes: exn list Unsynchronized.ref
+  val init: string -> string -> unit
 end;
 
 structure Isabelle_Process: ISABELLE_PROCESS =
@@ -25,6 +28,28 @@
 val _ = Markup.add_mode isabelle_processN YXML.output_markup;
 
 
+(* commands *)
+
+local
+
+val global_commands = Unsynchronized.ref (Symtab.empty: (string list -> unit) Symtab.table);
+
+in
+
+fun add_command name cmd = CRITICAL (fn () =>
+  Unsynchronized.change global_commands (fn cmds =>
+   (if not (Symtab.defined cmds name) then ()
+    else warning ("Redefining Isabelle process command " ^ quote name);
+    Symtab.update (name, cmd) cmds)));
+
+fun command name args =
+  (case Symtab.lookup (! global_commands) name of
+    NONE => error ("Undefined Isabelle process command " ^ quote name)
+  | SOME cmd => cmd args);
+
+end;
+
+
 (* message markup *)
 
 local
@@ -34,7 +59,7 @@
 fun message _ _ _ "" = ()
   | message out_stream ch props body =
       let
-        val header = YXML.string_of (XML.Elem ((ch, map (pairself YXML.binary_text) props), []));
+        val header = YXML.string_of (XML.Elem ((ch, map (pairself YXML.escape_controls) props), []));
         val msg = Symbol.STX ^ chunk header ^ chunk body;
       in TextIO.output (out_stream, msg) (*atomic output*) end;
 
@@ -57,16 +82,24 @@
   let
     val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream stream, IO.BLOCK_BUF);
     fun loop () =
-      (OS.Process.sleep (Time.fromMilliseconds 50); try TextIO.flushOut stream; loop ());
+      (OS.Process.sleep (Time.fromMilliseconds 20); try TextIO.flushOut stream; loop ());
   in loop end;
 
+fun rendezvous f fifo =
+  let
+    val path = File.platform_path (Path.explode fifo);
+    val result = f fifo;  (*should block until peer is ready*)
+    val _ =
+      if String.isSuffix "cygwin" ml_platform then ()  (*Cygwin 1.7: no proper blocking on open*)
+      else OS.FileSys.remove path;  (*prevent future access*)
+  in result end;
+
 in
 
-fun setup_channels out =
+fun setup_channels in_fifo out_fifo =
   let
-    val path = File.platform_path (Path.explode out);
-    val out_stream = TextIO.openOut path;  (*fifo blocks until reader is ready*)
-    val _ = OS.FileSys.remove path;  (*prevent alien access, indicate writer is ready*)
+    val in_stream = rendezvous TextIO.openIn in_fifo;
+    val out_stream = rendezvous TextIO.openOut out_fifo;
     val _ = Simple_Thread.fork false (auto_flush out_stream);
     val _ = Simple_Thread.fork false (auto_flush TextIO.stdOut);
     val _ = Simple_Thread.fork false (auto_flush TextIO.stdErr);
@@ -80,21 +113,72 @@
     Output.debug_fn    := standard_message out_stream "H";
     Output.priority_fn := ! Output.writeln_fn;
     Output.prompt_fn   := ignore;
-    out_stream
+    (in_stream, out_stream)
   end;
 
 end;
 
 
+(* protocol loop *)
+
+val crashes = Unsynchronized.ref ([]: exn list);
+
+local
+
+fun recover crash =
+  (CRITICAL (fn () => Unsynchronized.change crashes (cons crash));
+    warning "Recovering from Isabelle process crash -- see also Isabelle_Process.crashes");
+
+fun read_chunk stream len =
+  let
+    val n =
+      (case Int.fromString len of
+        SOME n => n
+      | NONE => error ("Isabelle process: malformed chunk header " ^ quote len));
+    val chunk = TextIO.inputN (stream, n);
+    val m = size chunk;
+  in
+    if m = n then chunk
+    else error ("Isabelle process: bad chunk (" ^ string_of_int m ^ " vs. " ^ string_of_int n ^ ")")
+  end;
+
+fun read_command stream =
+  (case TextIO.inputLine stream of
+    NONE => raise Runtime.TERMINATE
+  | SOME line => map (read_chunk stream) (space_explode "," line));
+
+fun run_command name args =
+  Runtime.debugging (command name) args
+    handle exn =>
+      error ("Isabelle process command failure: " ^ name ^ "\n" ^ ML_Compiler.exn_message exn);
+
+in
+
+fun loop stream =
+  let val continue =
+    (case read_command stream of
+      [] => (Output.error_msg "Isabelle process: no input"; true)
+    | name :: args => (run_command name args; true))
+    handle Runtime.TERMINATE => false
+      | exn => (Output.error_msg (ML_Compiler.exn_message exn) handle crash => recover crash; true);
+  in if continue then loop stream else () end;
+
+end;
+
+
 (* init *)
 
-fun init out =
- (Unsynchronized.change print_mode
-    (fold (update op =) [isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]);
-  setup_channels out |> init_message;
-  quick_and_dirty := true;  (* FIXME !? *)
-  Keyword.status ();
-  Output.status (Markup.markup Markup.ready "");
-  Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true});
+fun init in_fifo out_fifo =
+  let
+    val _ = Unsynchronized.change print_mode
+      (fold (update op =) [isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]);
+    val (in_stream, out_stream) = setup_channels in_fifo out_fifo;
+    val _ = init_message out_stream;
+    val _ = quick_and_dirty := true;  (* FIXME !? *)
+    val _ = Keyword.status ();
+    val _ = Output.status (Markup.markup Markup.ready "");
+    val _ = Context.set_thread_data NONE;
+    val _ = Simple_Thread.fork false (fn () => (loop in_stream; quit ()));
+  in () end;
 
 end;
diff -r 6daf896bca5e -r 01d2ef471ffe src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Wed Aug 11 12:04:06 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala	Wed Aug 11 12:50:33 2010 +0200
@@ -9,7 +9,7 @@
 
 import java.util.concurrent.LinkedBlockingQueue
 import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter,
-  InputStream, OutputStream, IOException}
+  InputStream, OutputStream, BufferedOutputStream, IOException}
 
 import scala.actors.Actor
 import Actor._
@@ -38,6 +38,7 @@
       kind == Markup.EXIT
     def is_system(kind: String) =
       kind == Markup.SYSTEM ||
+      kind == Markup.INPUT ||
       kind == Markup.STDIN ||
       kind == Markup.SIGNAL ||
       kind == Markup.EXIT ||
@@ -88,9 +89,8 @@
 
   /* process information */
 
-  @volatile private var proc: Process = null
-  @volatile private var closing = false
-  @volatile private var pid: String = null
+  @volatile private var proc: Option[Process] = None
+  @volatile private var pid: Option[String] = None
 
 
   /* results */
@@ -98,7 +98,7 @@
   private def put_result(kind: String, props: List[(String, String)], body: List[XML.Tree])
   {
     if (kind == Markup.INIT) {
-      for ((Markup.PID, p) <- props) pid = p
+      for ((Markup.PID, p) <- props) pid = Some(p)
     }
     receiver ! new Result(XML.Elem(Markup(kind, props), body))
   }
@@ -111,108 +111,80 @@
 
   /* signals */
 
-  def interrupt() = synchronized {
-    if (proc == null) error("Cannot interrupt Isabelle: no process")
-    if (pid == null) put_result(Markup.SYSTEM, "Cannot interrupt: unknown pid")
-    else {
-      try {
-        if (system.execute(true, "kill", "-INT", pid).waitFor == 0)
-          put_result(Markup.SIGNAL, "INT")
-        else
-          put_result(Markup.SYSTEM, "Cannot interrupt: kill command failed")
+  def interrupt()
+  {
+    if (proc.isEmpty) put_result(Markup.SYSTEM, "Cannot interrupt Isabelle: no process")
+    else
+      pid match {
+        case None => put_result(Markup.SYSTEM, "Cannot interrupt Isabelle: unknowd pid")
+        case Some(i) =>
+          try {
+            if (system.execute(true, "kill", "-INT", i).waitFor == 0)
+              put_result(Markup.SIGNAL, "INT")
+            else
+              put_result(Markup.SYSTEM, "Cannot interrupt Isabelle: kill command failed")
+          }
+          catch { case e: IOException => error("Cannot interrupt Isabelle: " + e.getMessage) }
       }
-      catch { case e: IOException => error("Cannot interrupt Isabelle: " + e.getMessage) }
-    }
   }
 
-  def kill() = synchronized {
-    if (proc == 0) error("Cannot kill Isabelle: no process")
-    else {
-      try_close()
-      Thread.sleep(500)  // FIXME property!?
-      put_result(Markup.SIGNAL, "KILL")
-      proc.destroy
-      proc = null
-      pid = null
+  def kill()
+  {
+    proc match {
+      case None => put_result(Markup.SYSTEM, "Cannot kill Isabelle: no process")
+      case Some(p) =>
+        close()
+        Thread.sleep(500)  // FIXME !?
+        put_result(Markup.SIGNAL, "KILL")
+        p.destroy
+        proc = None
+        pid = None
     }
   }
 
 
-  /* output being piped into the process */
 
-  private val output = new LinkedBlockingQueue[String]
+  /** stream actors **/
 
-  private def output_raw(text: String) = synchronized {
-    if (proc == null) error("Cannot output to Isabelle: no process")
-    if (closing) error("Cannot output to Isabelle: already closing")
-    output.put(text)
-  }
-
-  def output_sync(text: String) =
-    output_raw(" \\<^sync>\n; " + text + " \\<^sync>;\n")
+  case class Input_Text(text: String)
+  case class Input_Chunks(chunks: List[Array[Byte]])
+  case object Close
 
 
-  def command(text: String) =
-    output_sync("Isabelle.command " + Isabelle_Syntax.encode_string(text))
-
-  def command(props: List[(String, String)], text: String) =
-    output_sync("Isabelle.command " + Isabelle_Syntax.encode_properties(props) + " " +
-      Isabelle_Syntax.encode_string(text))
-
-  def ML_val(text: String) =
-    output_sync("ML_val " + Isabelle_Syntax.encode_string(text))
-
-  def ML_command(text: String) =
-    output_sync("ML_command " + Isabelle_Syntax.encode_string(text))
+  /* raw stdin */
 
-  def close() = synchronized {    // FIXME watchdog/timeout
-    output_raw("\u0000")
-    closing = true
-  }
-
-  def try_close() = synchronized {
-    if (proc != null && !closing) {
-      try { close() }
-      catch { case _: RuntimeException => }
-    }
-  }
-
-
-  /* stdin */
-
-  private class Stdin_Thread(out_stream: OutputStream) extends Thread("isabelle: stdin") {
-    override def run() = {
-      val writer = new BufferedWriter(new OutputStreamWriter(out_stream, Standard_System.charset))
+  private def stdin_actor(name: String, stream: OutputStream): Actor =
+    Library.thread_actor(name) {
+      val writer = new BufferedWriter(new OutputStreamWriter(stream, Standard_System.charset))
       var finished = false
       while (!finished) {
         try {
           //{{{
-          val s = output.take
-          if (s == "\u0000") {
-            writer.close
-            finished = true
-          }
-          else {
-            put_result(Markup.STDIN, s)
-            writer.write(s)
-            writer.flush
+          receive {
+            case Input_Text(text) =>
+              // FIXME echo input?!
+              writer.write(text)
+              writer.flush
+            case Close =>
+              writer.close
+              finished = true
+            case bad => System.err.println(name + ": ignoring bad message " + bad)
           }
           //}}}
         }
         catch {
-          case e: IOException => put_result(Markup.SYSTEM, "Stdin thread: " + e.getMessage)
+          case e: IOException => put_result(Markup.SYSTEM, name + ": " + e.getMessage)
         }
       }
-      put_result(Markup.SYSTEM, "Stdin thread terminated")
+      put_result(Markup.SYSTEM, name + " terminated")
     }
-  }
 
 
-  /* stdout */
+  /* raw stdout */
 
-  private class Stdout_Thread(in_stream: InputStream) extends Thread("isabelle: stdout") {
-    override def run() = {
-      val reader = new BufferedReader(new InputStreamReader(in_stream, Standard_System.charset))
+  private def stdout_actor(name: String, stream: InputStream): Actor =
+    Library.thread_actor(name) {
+      val reader = new BufferedReader(new InputStreamReader(stream, Standard_System.charset))
       var result = new StringBuilder(100)
 
       var finished = false
@@ -233,27 +205,54 @@
           else {
             reader.close
             finished = true
-            try_close()
+            close()
           }
           //}}}
         }
         catch {
-          case e: IOException => put_result(Markup.SYSTEM, "Stdout thread: " + e.getMessage)
+          case e: IOException => put_result(Markup.SYSTEM, name + ": " + e.getMessage)
         }
       }
-      put_result(Markup.SYSTEM, "Stdout thread terminated")
+      put_result(Markup.SYSTEM, name + " terminated")
     }
-  }
 
 
-  /* messages */
+  /* command input */
 
-  private class Message_Thread(fifo: String) extends Thread("isabelle: messages")
-  {
-    private class Protocol_Error(msg: String) extends Exception(msg)
-    override def run()
-    {
-      val stream = system.fifo_stream(fifo)
+  private def input_actor(name: String, raw_stream: OutputStream): Actor =
+    Library.thread_actor(name) {
+      val stream = new BufferedOutputStream(raw_stream)
+      var finished = false
+      while (!finished) {
+        try {
+          //{{{
+          receive {
+            case Input_Chunks(chunks) =>
+              stream.write(Standard_System.string_bytes(
+                  chunks.map(_.length).mkString("", ",", "\n")));
+              chunks.foreach(stream.write(_));
+              stream.flush
+            case Close =>
+              stream.close
+              finished = true
+            case bad => System.err.println(name + ": ignoring bad message " + bad)
+          }
+          //}}}
+        }
+        catch {
+          case e: IOException => put_result(Markup.SYSTEM, name + ": " + e.getMessage)
+        }
+      }
+      put_result(Markup.SYSTEM, name + " terminated")
+    }
+
+
+  /* message output */
+
+  private class Protocol_Error(msg: String) extends Exception(msg)
+
+  private def message_actor(name: String, stream: InputStream): Actor =
+    Library.thread_actor(name) {
       val default_buffer = new Array[Byte](65536)
       var c = -1
 
@@ -318,55 +317,64 @@
         }
       } while (c != -1)
       stream.close
-      try_close()
+      close()
+
+      put_result(Markup.SYSTEM, name + " terminated")
+    }
+
+
+
+  /** init **/
+
+  /* exec process */
+
+  private val in_fifo = system.mk_fifo()
+  private val out_fifo = system.mk_fifo()
+  private def rm_fifos() = { system.rm_fifo(in_fifo); system.rm_fifo(out_fifo) }
 
-      put_result(Markup.SYSTEM, "Message thread terminated")
+  try {
+    val cmdline =
+      List(system.getenv_strict("ISABELLE_PROCESS"), "-W", in_fifo + ":" + out_fifo) ++ args
+    proc = Some(system.execute(true, cmdline: _*))
+  }
+  catch {
+    case e: IOException =>
+      rm_fifos()
+      error("Failed to execute Isabelle process: " + e.getMessage)
+  }
+
+
+  /* I/O actors */
+
+  private val standard_input = stdin_actor("standard_input", proc.get.getOutputStream)
+  stdout_actor("standard_output", proc.get.getInputStream)
+
+  private val command_input = input_actor("command_input", system.fifo_output_stream(in_fifo))
+  message_actor("message_output", system.fifo_input_stream(out_fifo))
+
+
+  /* exit process */
+
+  Library.thread_actor("process_exit") {
+    proc match {
+      case None =>
+      case Some(p) =>
+        val rc = p.waitFor()
+        Thread.sleep(300)  // FIXME property!?
+        put_result(Markup.SYSTEM, "process_exit terminated")
+        put_result(Markup.EXIT, rc.toString)
     }
+    rm_fifos()
   }
 
 
 
-  /** main **/
-
-  {
-    /* messages */
+  /** main methods **/
 
-    val message_fifo = system.mk_fifo()
-    def rm_fifo() = system.rm_fifo(message_fifo)
-
-    val message_thread = new Message_Thread(message_fifo)
-    message_thread.start
-
-
-    /* exec process */
+  def input_raw(text: String): Unit = standard_input ! Input_Text(text)
 
-    try {
-      val cmdline = List(system.getenv_strict("ISABELLE_PROCESS"), "-W", message_fifo) ++ args
-      proc = system.execute(true, cmdline: _*)
-    }
-    catch {
-      case e: IOException =>
-        rm_fifo()
-        error("Failed to execute Isabelle process: " + e.getMessage)
-    }
-
-
-    /* stdin/stdout */
+  def input(name: String, args: String*): Unit =
+    command_input ! Input_Chunks((name :: args.toList).map(Standard_System.string_bytes))
 
-    new Stdin_Thread(proc.getOutputStream).start
-    new Stdout_Thread(proc.getInputStream).start
-
-
-    /* exit */
-
-    new Thread("isabelle: exit") {
-      override def run() = {
-        val rc = proc.waitFor()
-        Thread.sleep(300)  // FIXME property!?
-        put_result(Markup.SYSTEM, "Exit thread terminated")
-        put_result(Markup.EXIT, rc.toString)
-        rm_fifo()
-      }
-    }.start
-  }
+  def close(): Unit = command_input ! Close
 }
diff -r 6daf896bca5e -r 01d2ef471ffe src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Wed Aug 11 12:04:06 2010 +0200
+++ b/src/Pure/System/isabelle_system.scala	Wed Aug 11 12:50:33 2010 +0200
@@ -8,9 +8,8 @@
 
 import java.util.regex.Pattern
 import java.util.Locale
-import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream,
-  BufferedInputStream, FileInputStream, BufferedReader, InputStreamReader,
-  File, IOException}
+import java.io.{BufferedInputStream, FileInputStream, BufferedOutputStream, FileOutputStream,
+  OutputStream, File, IOException}
 import java.awt.{GraphicsEnvironment, Font}
 import java.awt.font.TextAttribute
 
@@ -288,12 +287,12 @@
     if (rc != 0) error(result)
   }
 
-  def fifo_stream(fifo: String): BufferedInputStream =
+  def fifo_input_stream(fifo: String): BufferedInputStream =
   {
-    // blocks until writer is ready
+    // block until peer is ready
     val stream =
-      if (Platform.is_windows) {
-        val proc = execute(false, "cat", fifo)
+      if (Platform.is_windows) { // Cygwin fifo as Windows/Java input stream
+        val proc = execute(false, expand_path("$ISABELLE_HOME/lib/scripts/raw_dump"), fifo, "-")
         proc.getOutputStream.close
         proc.getErrorStream.close
         proc.getInputStream
@@ -302,6 +301,27 @@
     new BufferedInputStream(stream)
   }
 
+  def fifo_output_stream(fifo: String): BufferedOutputStream =
+  {
+    // block until peer is ready
+    val stream =
+      if (Platform.is_windows) { // Cygwin fifo as Windows/Java output stream
+        val proc = execute(false, expand_path("$ISABELLE_HOME/lib/scripts/raw_dump"), "-", fifo)
+        proc.getInputStream.close
+        proc.getErrorStream.close
+        val out = proc.getOutputStream
+        new OutputStream {
+          override def close() { out.close(); proc.waitFor() }
+          override def flush() { out.flush() }
+          override def write(b: Array[Byte]) { out.write(b) }
+          override def write(b: Array[Byte], off: Int, len: Int) { out.write(b, off, len) }
+          override def write(b: Int) { out.write(b) }
+        }
+      }
+      else new FileOutputStream(fifo)
+    new BufferedOutputStream(stream)
+  }
+
 
 
   /** Isabelle resources **/
diff -r 6daf896bca5e -r 01d2ef471ffe src/Pure/System/isar.ML
--- a/src/Pure/System/isar.ML	Wed Aug 11 12:04:06 2010 +0200
+++ b/src/Pure/System/isar.ML	Wed Aug 11 12:50:33 2010 +0200
@@ -18,7 +18,8 @@
   val kill: unit -> unit
   val kill_proof: unit -> unit
   val crashes: exn list Unsynchronized.ref
-  val toplevel_loop: {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
+  val toplevel_loop: TextIO.instream ->
+    {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
   val loop: unit -> unit
   val main: unit -> unit
 end;
@@ -126,25 +127,27 @@
         handle crash =>
           (CRITICAL (fn () => Unsynchronized.change crashes (cons crash));
             warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
-          raw_loop secure src)
+        raw_loop secure src)
   end;
 
 in
 
-fun toplevel_loop {init = do_init, welcome, sync, secure} =
+fun toplevel_loop in_stream {init = do_init, welcome, sync, secure} =
  (Context.set_thread_data NONE;
   Secure.Isar_setup ();
   if do_init then init () else ();
   if welcome then writeln (Session.welcome ()) else ();
-  uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar sync)) ());
+  uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar in_stream sync)) ());
 
 end;
 
 fun loop () =
-  toplevel_loop {init = false, welcome = false, sync = false, secure = Secure.is_secure ()};
+  toplevel_loop TextIO.stdIn
+    {init = false, welcome = false, sync = false, secure = Secure.is_secure ()};
 
 fun main () =
-  toplevel_loop {init = true, welcome = true, sync = false, secure = Secure.is_secure ()};
+  toplevel_loop TextIO.stdIn
+    {init = true, welcome = true, sync = false, secure = Secure.is_secure ()};
 
 
 
diff -r 6daf896bca5e -r 01d2ef471ffe src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Wed Aug 11 12:04:06 2010 +0200
+++ b/src/Pure/System/session.scala	Wed Aug 11 12:50:33 2010 +0200
@@ -334,6 +334,7 @@
             val new_change = new Document.Change(new_id, Some(old_change), edits, result)
             history = new_change
             new_change.result.map(_ => session_actor ! new_change)
+            reply(())
 
           case bad => System.err.println("editor_model: ignoring bad message " + bad)
         }
@@ -352,5 +353,6 @@
   def stop() { session_actor ! Stop }
 
   def current_change(): Document.Change = editor_history.current_change()
-  def edit_document(edits: List[Document.Node_Text_Edit]) { editor_history ! Edit_Document(edits) }
+
+  def edit_document(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Document(edits) }
 }
diff -r 6daf896bca5e -r 01d2ef471ffe src/Pure/System/standard_system.scala
--- a/src/Pure/System/standard_system.scala	Wed Aug 11 12:04:06 2010 +0200
+++ b/src/Pure/System/standard_system.scala	Wed Aug 11 12:50:33 2010 +0200
@@ -19,9 +19,13 @@
 
 object Standard_System
 {
+  /* UTF-8 charset */
+
   val charset = "UTF-8"
   def codec(): Codec = Codec(charset)
 
+  def string_bytes(s: String): Array[Byte] = s.getBytes(charset)
+
 
   /* permissive UTF-8 decoding */
 
diff -r 6daf896bca5e -r 01d2ef471ffe src/Pure/build-jars
--- a/src/Pure/build-jars	Wed Aug 11 12:04:06 2010 +0200
+++ b/src/Pure/build-jars	Wed Aug 11 12:50:33 2010 +0200
@@ -31,6 +31,7 @@
   General/scan.scala
   General/symbol.scala
   General/xml.scala
+  General/xml_data.scala
   General/yxml.scala
   Isar/isar_document.scala
   Isar/keyword.scala
diff -r 6daf896bca5e -r 01d2ef471ffe src/Pure/library.scala
--- a/src/Pure/library.scala	Wed Aug 11 12:04:06 2010 +0200
+++ b/src/Pure/library.scala	Wed Aug 11 12:50:33 2010 +0200
@@ -6,11 +6,12 @@
 
 package isabelle
 
-import java.lang.System
+
+import java.lang.{System, Thread}
 import java.awt.Component
 import javax.swing.JOptionPane
 
-
+import scala.actors.Actor
 import scala.swing.ComboBox
 import scala.swing.event.SelectionChanged
 
@@ -138,4 +139,15 @@
         ((stop - start).toDouble / 1000000) + "ms elapsed time")
     Exn.release(result)
   }
+
+
+  /* thread as actor */
+
+  def thread_actor(name: String)(body: => Unit): Actor =
+  {
+    val actor = Future.promise[Actor]
+    val thread = new Thread(name) { override def run() = { actor.fulfill(Actor.self); body } }
+    thread.start
+    actor.join
+  }
 }
diff -r 6daf896bca5e -r 01d2ef471ffe src/Tools/jEdit/dist-template/etc/settings
--- a/src/Tools/jEdit/dist-template/etc/settings	Wed Aug 11 12:04:06 2010 +0200
+++ b/src/Tools/jEdit/dist-template/etc/settings	Wed Aug 11 12:50:33 2010 +0200
@@ -3,10 +3,10 @@
 JEDIT_HOME="$COMPONENT"
 JEDIT_SETTINGS="$ISABELLE_HOME_USER/jedit"
 
-JEDIT_APPLE_PROPERTIES="-Dapple.laf.useScreenMenuBar=true -Dcom.apple.mrj.application.apple.menu.about.name=Isabelle/jEdit"
-JEDIT_JAVA_OPTIONS="-Xms128m -Xmx512m -Xss2m $JEDIT_APPLE_PROPERTIES"
-#JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx1024m -Xss4m $JEDIT_APPLE_PROPERTIES"
 JEDIT_OPTIONS="-reuseview -noserver -nobackground"
+JEDIT_JAVA_OPTIONS="-Xms128m -Xmx512m -Xss2m -Dactors.corePoolSize=4"
+#JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx1024m -Xss4m -Dactors.corePoolSize=8"
+JEDIT_SYSTEM_OPTIONS="-Dapple.laf.useScreenMenuBar=true -Dcom.apple.mrj.application.apple.menu.about.name=Isabelle/jEdit"
 
 JEDIT_STYLE_SHEETS="$ISABELLE_HOME/lib/html/isabelle.css:$JEDIT_HOME/etc/isabelle-jedit.css:$ISABELLE_HOME_USER/etc/isabelle.css:$ISABELLE_HOME_USER/etc/isabelle-jedit.css"
 
diff -r 6daf896bca5e -r 01d2ef471ffe src/Tools/jEdit/dist-template/lib/Tools/jedit
--- a/src/Tools/jEdit/dist-template/lib/Tools/jedit	Wed Aug 11 12:04:06 2010 +0200
+++ b/src/Tools/jEdit/dist-template/lib/Tools/jedit	Wed Aug 11 12:50:33 2010 +0200
@@ -76,7 +76,7 @@
   done
 }
 
-declare -a JAVA_ARGS; eval "JAVA_ARGS=($JEDIT_JAVA_OPTIONS)"
+declare -a JAVA_ARGS; eval "JAVA_ARGS=($JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS)"
 [ -n "$SCALA_HOME" ] && JAVA_ARGS["${#JAVA_ARGS[@]}"]="-Dscala.home=$SCALA_HOME"
 
 declare -a ARGS; eval "ARGS=($JEDIT_OPTIONS)"
diff -r 6daf896bca5e -r 01d2ef471ffe src/Tools/jEdit/dist-template/properties/jedit.props
--- a/src/Tools/jEdit/dist-template/properties/jedit.props	Wed Aug 11 12:04:06 2010 +0200
+++ b/src/Tools/jEdit/dist-template/properties/jedit.props	Wed Aug 11 12:50:33 2010 +0200
@@ -185,6 +185,7 @@
 isabelle.activate.shortcut=CS+ENTER
 line-end.shortcut=END
 line-home.shortcut=HOME
+lookAndFeel=com.sun.java.swing.plaf.nimbus.NimbusLookAndFeel
 mode.isabelle.sidekick.showStatusWindow.label=true
 print.font=IsabelleText
 sidekick-tree.dock-position=right