merged, resolving conflict in src/Pure/IsaMakefile concerning General/xml_data.ML;
--- 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
--- 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
--- 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
--- 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"
--- /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;
+
--- 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)
--- 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)+
--- 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
--- 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 -
--- 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))))"
--- 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 =
--- 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"
--- 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);
--- 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;
--- 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 ++= "<"
- case '>' => s ++= ">"
- case '&' => s ++= "&"
- case '"' => s ++= """
- case '\'' => s ++= "'"
- 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 ++= "<"
+ case '>' => s ++= ">"
+ case '&' => s ++= "&"
+ case '"' => s ++= """
+ case '\'' => s ++= "'"
+ 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 */
--- /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;
+
--- /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)
+ }
+}
--- 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;
--- 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)) }
--- 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 \
--- 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;
--- 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))
}
}
--- 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;
--- 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 *)
--- 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
--- 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 *)
--- 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;
--- 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
}
--- 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 **/
--- 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 ()};
--- 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) }
}
--- 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 */
--- 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
--- 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
+ }
}
--- 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"
--- 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)"
--- 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