# HG changeset patch
# User nipkow
# Date 1344614626 -7200
# Node ID 4218d7b5d892b4969c196d93649e1c51715af5dd
# Parent  80ad6e0e147f5a484cf62b2f30b1614529c5d17a# Parent  ff570720ba1c73015f08b34abc2f61b8e868ee66
merged

diff -r ff570720ba1c -r 4218d7b5d892 etc/isabelle.css
--- a/etc/isabelle.css	Fri Aug 10 17:17:05 2012 +0200
+++ b/etc/isabelle.css	Fri Aug 10 18:03:46 2012 +0200
@@ -42,7 +42,5 @@
 .verbatim       { color: #00008B; }
 .comment        { color: #8B0000; }
 .control        { background-color: #FF6A6A; }
-.malformed      { background-color: #FF6A6A; }
+.bad            { background-color: #FF6A6A; }
 
-.malformed_span { background-color: #FF6A6A; }
-
diff -r ff570720ba1c -r 4218d7b5d892 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Fri Aug 10 17:17:05 2012 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Aug 10 18:03:46 2012 +0200
@@ -26,7 +26,8 @@
 lemma fps_nth_Abs_fps [simp]: "Abs_fps f $ n = f n"
   by (simp add: Abs_fps_inverse)
 
-text{* Definition of the basic elements 0 and 1 and the basic operations of addition, negation and multiplication *}
+text{* Definition of the basic elements 0 and 1 and the basic operations of addition,
+  negation and multiplication *}
 
 instantiation fps :: (zero) zero
 begin
@@ -335,10 +336,12 @@
 lemma fps_const_mult[simp]: "fps_const (c::'a\<Colon>ring) * fps_const d = fps_const (c * d)"
   by (simp add: fps_eq_iff fps_mult_nth setsum_0')
 
-lemma fps_const_add_left: "fps_const (c::'a\<Colon>monoid_add) + f = Abs_fps (\<lambda>n. if n = 0 then c + f$0 else f$n)"
+lemma fps_const_add_left: "fps_const (c::'a\<Colon>monoid_add) + f =
+    Abs_fps (\<lambda>n. if n = 0 then c + f$0 else f$n)"
   by (simp add: fps_ext)
 
-lemma fps_const_add_right: "f + fps_const (c::'a\<Colon>monoid_add) = Abs_fps (\<lambda>n. if n = 0 then f$0 + c else f$n)"
+lemma fps_const_add_right: "f + fps_const (c::'a\<Colon>monoid_add) =
+    Abs_fps (\<lambda>n. if n = 0 then f$0 + c else f$n)"
   by (simp add: fps_ext)
 
 lemma fps_const_mult_left: "fps_const (c::'a\<Colon>semiring_0) * f = Abs_fps (\<lambda>n. c * f$n)"
@@ -393,7 +396,7 @@
 instance fps :: (idom) idom ..
 
 lemma numeral_fps_const: "numeral k = fps_const (numeral k)"
-  by (induct k, simp_all only: numeral.simps fps_const_1_eq_1
+  by (induct k) (simp_all only: numeral.simps fps_const_1_eq_1
     fps_const_add [symmetric])
 
 lemma neg_numeral_fps_const: "neg_numeral k = fps_const (neg_numeral k)"
@@ -402,7 +405,7 @@
 subsection{* The eXtractor series X*}
 
 lemma minus_one_power_iff: "(- (1::'a :: {comm_ring_1})) ^ n = (if even n then 1 else - 1)"
-  by (induct n, auto)
+  by (induct n) auto
 
 definition "X = Abs_fps (\<lambda>n. if n = 1 then 1 else 0)"
 lemma X_mult_nth[simp]: "(X * (f :: ('a::semiring_1) fps)) $n = (if n = 0 then 0 else f $ (n - 1))"
@@ -417,7 +420,8 @@
   ultimately show ?thesis by blast
 qed
 
-lemma X_mult_right_nth[simp]: "((f :: ('a::comm_semiring_1) fps) * X) $n = (if n = 0 then 0 else f $ (n - 1))"
+lemma X_mult_right_nth[simp]:
+    "((f :: ('a::comm_semiring_1) fps) * X) $n = (if n = 0 then 0 else f $ (n - 1))"
   by (metis X_mult_nth mult_commute)
 
 lemma X_power_iff: "X^k = Abs_fps (\<lambda>n. if n = k then (1::'a::comm_ring_1) else 0)"
@@ -433,13 +437,17 @@
   then show ?case by (simp add: fps_eq_iff)
 qed
 
-lemma X_power_mult_nth: "(X^k * (f :: ('a::comm_ring_1) fps)) $n = (if n < k then 0 else f $ (n - k))"
+lemma X_power_mult_nth:
+    "(X^k * (f :: ('a::comm_ring_1) fps)) $n = (if n < k then 0 else f $ (n - k))"
   apply (induct k arbitrary: n)
   apply (simp)
   unfolding power_Suc mult_assoc
-  by (case_tac n, auto)
-
-lemma X_power_mult_right_nth: "((f :: ('a::comm_ring_1) fps) * X^k) $n = (if n < k then 0 else f $ (n - k))"
+  apply (case_tac n)
+  apply auto
+  done
+
+lemma X_power_mult_right_nth:
+    "((f :: ('a::comm_ring_1) fps) * X^k) $n = (if n < k then 0 else f $ (n - k))"
   by (metis X_power_mult_nth mult_commute)
 
 
@@ -448,10 +456,12 @@
 subsection{* Formal Power series form a metric space *}
 
 definition (in dist) ball_def: "ball x r = {y. dist y x < r}"
+
 instantiation fps :: (comm_ring_1) dist
 begin
 
-definition dist_fps_def: "dist (a::'a fps) b = (if (\<exists>n. a$n \<noteq> b$n) then inverse (2 ^ The (leastP (\<lambda>n. a$n \<noteq> b$n))) else 0)"
+definition dist_fps_def:
+  "dist (a::'a fps) b = (if (\<exists>n. a$n \<noteq> b$n) then inverse (2 ^ The (leastP (\<lambda>n. a$n \<noteq> b$n))) else 0)"
 
 lemma dist_fps_ge0: "dist (a::'a fps) b \<ge> 0"
   by (simp add: dist_fps_def)
@@ -460,8 +470,11 @@
   apply (auto simp add: dist_fps_def)
   apply (rule cong[OF refl, where x="(\<lambda>n\<Colon>nat. a $ n \<noteq> b $ n)"])
   apply (rule ext)
-  by auto
+  apply auto
+  done
+
 instance ..
+
 end
 
 lemma fps_nonzero_least_unique: assumes a0: "a \<noteq> 0"
@@ -481,10 +494,11 @@
   ultimately show ?thesis by blast
 qed
 
-lemma fps_eq_least_unique: assumes ab: "(a::('a::ab_group_add) fps) \<noteq> b"
+lemma fps_eq_least_unique:
+  assumes ab: "(a::('a::ab_group_add) fps) \<noteq> b"
   shows "\<exists>! n. leastP (\<lambda>n. a$n \<noteq> b$n) n"
-using fps_nonzero_least_unique[of "a - b"] ab
-by auto
+  using fps_nonzero_least_unique[of "a - b"] ab
+  by auto
 
 instantiation fps :: (comm_ring_1) metric_space
 begin
@@ -497,25 +511,36 @@
   show "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
     by (auto simp add: open_fps_def ball_def subset_eq)
 next
-{  fix a b :: "'a fps"
-  {assume ab: "a = b"
-   then have "\<not> (\<exists>n. a$n \<noteq> b$n)" by simp
-   then have "dist a b = 0" by (simp add: dist_fps_def)}
- moreover
- {assume d: "dist a b = 0"
-   then have "\<forall>n. a$n = b$n" 
-     by - (rule ccontr, simp add: dist_fps_def)
-   then have "a = b" by (simp add: fps_eq_iff)}
- ultimately show "dist a b =0 \<longleftrightarrow> a = b" by blast}
-note th = this
-from th have th'[simp]: "\<And>a::'a fps. dist a a = 0" by simp
+  {
+    fix a b :: "'a fps"
+    {
+      assume ab: "a = b"
+      then have "\<not> (\<exists>n. a$n \<noteq> b$n)" by simp
+      then have "dist a b = 0" by (simp add: dist_fps_def)
+    }
+    moreover
+    {
+      assume d: "dist a b = 0"
+      then have "\<forall>n. a$n = b$n" 
+        by - (rule ccontr, simp add: dist_fps_def)
+      then have "a = b" by (simp add: fps_eq_iff)
+    }
+    ultimately show "dist a b =0 \<longleftrightarrow> a = b" by blast
+  }
+  note th = this
+  from th have th'[simp]: "\<And>a::'a fps. dist a a = 0" by simp
   fix a b c :: "'a fps"
-  {assume ab: "a = b" then have d0: "dist a b = 0"  unfolding th .
+  {
+    assume ab: "a = b" then have d0: "dist a b = 0"  unfolding th .
     then have "dist a b \<le> dist a c + dist b c" 
-      using dist_fps_ge0[of a c] dist_fps_ge0[of b c] by simp}
+      using dist_fps_ge0[of a c] dist_fps_ge0[of b c] by simp
+  }
   moreover
-  {assume c: "c = a \<or> c = b" then have "dist a b \<le> dist a c + dist b c"
-      by (cases "c=a", simp_all add: th dist_fps_sym) }
+  {
+    assume c: "c = a \<or> c = b"
+    then have "dist a b \<le> dist a c + dist b c"
+      by (cases "c=a") (simp_all add: th dist_fps_sym)
+  }
   moreover
   {assume ab: "a \<noteq> b" and ac: "a \<noteq> c" and bc: "b \<noteq> c"
     let ?P = "\<lambda>a b n. a$n \<noteq> b$n"
@@ -591,9 +616,12 @@
   by (simp add: X_power_iff)
  
 
-lemma fps_sum_rep_nth: "(setsum (%i. fps_const(a$i)*X^i) {0..m})$n = (if n \<le> m then a$n else (0::'a::comm_ring_1))"
-  apply (auto simp add: fps_eq_iff fps_setsum_nth X_power_nth cond_application_beta cond_value_iff  cong del: if_weak_cong)
-  by (simp add: setsum_delta')
+lemma fps_sum_rep_nth: "(setsum (%i. fps_const(a$i)*X^i) {0..m})$n =
+    (if n \<le> m then a$n else (0::'a::comm_ring_1))"
+  apply (auto simp add: fps_eq_iff fps_setsum_nth X_power_nth cond_application_beta cond_value_iff
+    cong del: if_weak_cong)
+  apply (simp add: setsum_delta')
+  done
   
 lemma fps_notation: 
   "(%n. setsum (%i. fps_const(a$i) * X^i) {0..n}) ----> a" (is "?s ----> a")
@@ -702,7 +730,8 @@
   ultimately show ?thesis by blast
 qed
 
-lemma fps_inverse_idempotent[intro]: assumes f0: "f$0 \<noteq> (0::'a::field)"
+lemma fps_inverse_idempotent[intro]:
+  assumes f0: "f$0 \<noteq> (0::'a::field)"
   shows "inverse (inverse f) = f"
 proof-
   from f0 have if0: "inverse f $ 0 \<noteq> 0" by simp
@@ -711,7 +740,8 @@
   then show ?thesis using f0 unfolding mult_cancel_left by simp
 qed
 
-lemma fps_inverse_unique: assumes f0: "f$0 \<noteq> (0::'a::field)" and fg: "f*g = 1"
+lemma fps_inverse_unique:
+  assumes f0: "f$0 \<noteq> (0::'a::field)" and fg: "f*g = 1"
   shows "inverse f = g"
 proof-
   from inverse_mult_eq_1[OF f0] fg
@@ -748,9 +778,12 @@
 
 definition "fps_deriv f = Abs_fps (\<lambda>n. of_nat (n + 1) * f $ (n + 1))"
 
-lemma fps_deriv_nth[simp]: "fps_deriv f $ n = of_nat (n +1) * f $ (n+1)" by (simp add: fps_deriv_def)
-
-lemma fps_deriv_linear[simp]: "fps_deriv (fps_const (a::'a::comm_semiring_1) * f + fps_const b * g) = fps_const a * fps_deriv f + fps_const b * fps_deriv g"
+lemma fps_deriv_nth[simp]: "fps_deriv f $ n = of_nat (n +1) * f $ (n+1)"
+  by (simp add: fps_deriv_def)
+
+lemma fps_deriv_linear[simp]:
+  "fps_deriv (fps_const (a::'a::comm_semiring_1) * f + fps_const b * g) =
+    fps_const a * fps_deriv f + fps_const b * fps_deriv g"
   unfolding fps_eq_iff fps_add_nth  fps_const_mult_left fps_deriv_nth by (simp add: field_simps)
 
 lemma fps_deriv_mult[simp]:
@@ -821,7 +854,8 @@
 lemma fps_deriv_const[simp]: "fps_deriv (fps_const c) = 0"
   by (simp add: fps_ext fps_deriv_def fps_const_def)
 
-lemma fps_deriv_mult_const_left[simp]: "fps_deriv (fps_const (c::'a::comm_ring_1) * f) = fps_const c * fps_deriv f"
+lemma fps_deriv_mult_const_left[simp]:
+    "fps_deriv (fps_const (c::'a::comm_ring_1) * f) = fps_const c * fps_deriv f"
   by simp
 
 lemma fps_deriv_0[simp]: "fps_deriv 0 = 0"
@@ -830,19 +864,24 @@
 lemma fps_deriv_1[simp]: "fps_deriv 1 = 0"
   by (simp add: fps_deriv_def fps_eq_iff )
 
-lemma fps_deriv_mult_const_right[simp]: "fps_deriv (f * fps_const (c::'a::comm_ring_1)) = fps_deriv f * fps_const c"
+lemma fps_deriv_mult_const_right[simp]:
+    "fps_deriv (f * fps_const (c::'a::comm_ring_1)) = fps_deriv f * fps_const c"
   by simp
 
-lemma fps_deriv_setsum: "fps_deriv (setsum f S) = setsum (\<lambda>i. fps_deriv (f i :: ('a::comm_ring_1) fps)) S"
+lemma fps_deriv_setsum:
+  "fps_deriv (setsum f S) = setsum (\<lambda>i. fps_deriv (f i :: ('a::comm_ring_1) fps)) S"
 proof-
-  {assume "\<not> finite S" hence ?thesis by simp}
+  { assume "\<not> finite S" hence ?thesis by simp }
   moreover
-  {assume fS: "finite S"
-    have ?thesis  by (induct rule: finite_induct[OF fS], simp_all)}
+  {
+    assume fS: "finite S"
+    have ?thesis  by (induct rule: finite_induct[OF fS]) simp_all
+  }
   ultimately show ?thesis by blast
 qed
 
-lemma fps_deriv_eq_0_iff[simp]: "fps_deriv f = 0 \<longleftrightarrow> (f = fps_const (f$0 :: 'a::{idom,semiring_char_0}))"
+lemma fps_deriv_eq_0_iff[simp]:
+  "fps_deriv f = 0 \<longleftrightarrow> (f = fps_const (f$0 :: 'a::{idom,semiring_char_0}))"
 proof-
   {assume "f= fps_const (f$0)" hence "fps_deriv f = fps_deriv (fps_const (f$0))" by simp
     hence "fps_deriv f = 0" by simp }
@@ -866,60 +905,76 @@
   finally show ?thesis by (simp add: field_simps)
 qed
 
-lemma fps_deriv_eq_iff_ex: "(fps_deriv f = fps_deriv g) \<longleftrightarrow> (\<exists>(c::'a::{idom,semiring_char_0}). f = fps_const c + g)"
-  apply auto unfolding fps_deriv_eq_iff by blast
-
-
-fun fps_nth_deriv :: "nat \<Rightarrow> ('a::semiring_1) fps \<Rightarrow> 'a fps" where
+lemma fps_deriv_eq_iff_ex:
+  "(fps_deriv f = fps_deriv g) \<longleftrightarrow> (\<exists>(c::'a::{idom,semiring_char_0}). f = fps_const c + g)"
+  apply auto unfolding fps_deriv_eq_iff
+  apply blast
+  done
+
+
+fun fps_nth_deriv :: "nat \<Rightarrow> ('a::semiring_1) fps \<Rightarrow> 'a fps"
+where
   "fps_nth_deriv 0 f = f"
 | "fps_nth_deriv (Suc n) f = fps_nth_deriv n (fps_deriv f)"
 
 lemma fps_nth_deriv_commute: "fps_nth_deriv (Suc n) f = fps_deriv (fps_nth_deriv n f)"
-  by (induct n arbitrary: f, auto)
-
-lemma fps_nth_deriv_linear[simp]: "fps_nth_deriv n (fps_const (a::'a::comm_semiring_1) * f + fps_const b * g) = fps_const a * fps_nth_deriv n f + fps_const b * fps_nth_deriv n g"
-  by (induct n arbitrary: f g, auto simp add: fps_nth_deriv_commute)
-
-lemma fps_nth_deriv_neg[simp]: "fps_nth_deriv n (- (f:: ('a:: comm_ring_1) fps)) = - (fps_nth_deriv n f)"
-  by (induct n arbitrary: f, simp_all)
-
-lemma fps_nth_deriv_add[simp]: "fps_nth_deriv n ((f:: ('a::comm_ring_1) fps) + g) = fps_nth_deriv n f + fps_nth_deriv n g"
+  by (induct n arbitrary: f) auto
+
+lemma fps_nth_deriv_linear[simp]:
+  "fps_nth_deriv n (fps_const (a::'a::comm_semiring_1) * f + fps_const b * g) =
+    fps_const a * fps_nth_deriv n f + fps_const b * fps_nth_deriv n g"
+  by (induct n arbitrary: f g) (auto simp add: fps_nth_deriv_commute)
+
+lemma fps_nth_deriv_neg[simp]:
+  "fps_nth_deriv n (- (f:: ('a:: comm_ring_1) fps)) = - (fps_nth_deriv n f)"
+  by (induct n arbitrary: f) simp_all
+
+lemma fps_nth_deriv_add[simp]:
+  "fps_nth_deriv n ((f:: ('a::comm_ring_1) fps) + g) = fps_nth_deriv n f + fps_nth_deriv n g"
   using fps_nth_deriv_linear[of n 1 f 1 g] by simp
 
-lemma fps_nth_deriv_sub[simp]: "fps_nth_deriv n ((f:: ('a::comm_ring_1) fps) - g) = fps_nth_deriv n f - fps_nth_deriv n g"
+lemma fps_nth_deriv_sub[simp]:
+  "fps_nth_deriv n ((f:: ('a::comm_ring_1) fps) - g) = fps_nth_deriv n f - fps_nth_deriv n g"
   unfolding diff_minus fps_nth_deriv_add by simp
 
 lemma fps_nth_deriv_0[simp]: "fps_nth_deriv n 0 = 0"
-  by (induct n, simp_all )
+  by (induct n) simp_all
 
 lemma fps_nth_deriv_1[simp]: "fps_nth_deriv n 1 = (if n = 0 then 1 else 0)"
-  by (induct n, simp_all )
-
-lemma fps_nth_deriv_const[simp]: "fps_nth_deriv n (fps_const c) = (if n = 0 then fps_const c else 0)"
-  by (cases n, simp_all)
-
-lemma fps_nth_deriv_mult_const_left[simp]: "fps_nth_deriv n (fps_const (c::'a::comm_ring_1) * f) = fps_const c * fps_nth_deriv n f"
+  by (induct n) simp_all
+
+lemma fps_nth_deriv_const[simp]:
+  "fps_nth_deriv n (fps_const c) = (if n = 0 then fps_const c else 0)"
+  by (cases n) simp_all
+
+lemma fps_nth_deriv_mult_const_left[simp]:
+  "fps_nth_deriv n (fps_const (c::'a::comm_ring_1) * f) = fps_const c * fps_nth_deriv n f"
   using fps_nth_deriv_linear[of n "c" f 0 0 ] by simp
 
-lemma fps_nth_deriv_mult_const_right[simp]: "fps_nth_deriv n (f * fps_const (c::'a::comm_ring_1)) = fps_nth_deriv n f * fps_const c"
+lemma fps_nth_deriv_mult_const_right[simp]:
+  "fps_nth_deriv n (f * fps_const (c::'a::comm_ring_1)) = fps_nth_deriv n f * fps_const c"
   using fps_nth_deriv_linear[of n "c" f 0 0] by (simp add: mult_commute)
 
-lemma fps_nth_deriv_setsum: "fps_nth_deriv n (setsum f S) = setsum (\<lambda>i. fps_nth_deriv n (f i :: ('a::comm_ring_1) fps)) S"
+lemma fps_nth_deriv_setsum:
+  "fps_nth_deriv n (setsum f S) = setsum (\<lambda>i. fps_nth_deriv n (f i :: ('a::comm_ring_1) fps)) S"
 proof-
-  {assume "\<not> finite S" hence ?thesis by simp}
+  { assume "\<not> finite S" hence ?thesis by simp }
   moreover
-  {assume fS: "finite S"
-    have ?thesis  by (induct rule: finite_induct[OF fS], simp_all)}
+  {
+    assume fS: "finite S"
+    have ?thesis  by (induct rule: finite_induct[OF fS]) simp_all
+  }
   ultimately show ?thesis by blast
 qed
 
-lemma fps_deriv_maclauren_0: "(fps_nth_deriv k (f:: ('a::comm_semiring_1) fps)) $ 0 = of_nat (fact k) * f$(k)"
+lemma fps_deriv_maclauren_0:
+  "(fps_nth_deriv k (f:: ('a::comm_semiring_1) fps)) $ 0 = of_nat (fact k) * f$(k)"
   by (induct k arbitrary: f) (auto simp add: field_simps of_nat_mult)
 
 subsection {* Powers*}
 
 lemma fps_power_zeroth_eq_one: "a$0 =1 \<Longrightarrow> a^n $ 0 = (1::'a::semiring_1)"
-  by (induct n, auto simp add: expand_fps_eq fps_mult_nth)
+  by (induct n) (auto simp add: expand_fps_eq fps_mult_nth)
 
 lemma fps_power_first_eq: "(a:: 'a::comm_ring_1 fps)$0 =1 \<Longrightarrow> a^n $ 1 = of_nat n * a$1"
 proof(induct n)
@@ -932,19 +987,21 @@
 qed
 
 lemma startsby_one_power:"a $ 0 = (1::'a::comm_ring_1) \<Longrightarrow> a^n $ 0 = 1"
-  by (induct n, auto simp add: fps_mult_nth)
+  by (induct n) (auto simp add: fps_mult_nth)
 
 lemma startsby_zero_power:"a $0 = (0::'a::comm_ring_1) \<Longrightarrow> n > 0 \<Longrightarrow> a^n $0 = 0"
-  by (induct n, auto simp add: fps_mult_nth)
+  by (induct n) (auto simp add: fps_mult_nth)
 
 lemma startsby_power:"a $0 = (v::'a::{comm_ring_1}) \<Longrightarrow> a^n $0 = v^n"
-  by (induct n, auto simp add: fps_mult_nth power_Suc)
+  by (induct n) (auto simp add: fps_mult_nth power_Suc)
 
 lemma startsby_zero_power_iff[simp]:
   "a^n $0 = (0::'a::{idom}) \<longleftrightarrow> (n \<noteq> 0 \<and> a$0 = 0)"
 apply (rule iffI)
-apply (induct n, auto simp add: power_Suc fps_mult_nth)
-by (rule startsby_zero_power, simp_all)
+apply (induct n)
+apply (auto simp add: fps_mult_nth)
+apply (rule startsby_zero_power, simp_all)
+done
 
 lemma startsby_zero_power_prefix:
   assumes a0: "a $0 = (0::'a::idom)"
@@ -1029,9 +1086,13 @@
   ultimately show ?thesis by blast
 qed
 
-lemma fps_deriv_power: "fps_deriv (a ^ n) = fps_const (of_nat n :: 'a:: comm_ring_1) * fps_deriv a * a ^ (n - 1)"
-  apply (induct n, auto simp add: power_Suc field_simps fps_const_add[symmetric] simp del: fps_const_add)
-  by (case_tac n, auto simp add: power_Suc field_simps)
+lemma fps_deriv_power:
+    "fps_deriv (a ^ n) = fps_const (of_nat n :: 'a:: comm_ring_1) * fps_deriv a * a ^ (n - 1)"
+  apply (induct n)
+  apply (auto simp add: power_Suc field_simps fps_const_add[symmetric] simp del: fps_const_add)
+  apply (case_tac n)
+  apply (auto simp add: power_Suc field_simps)
+  done
 
 lemma fps_inverse_deriv:
   fixes a:: "('a :: field) fps"
@@ -1079,8 +1140,8 @@
   assumes a0: "a$0 \<noteq> 0"
   shows "fps_deriv (inverse a) = - fps_deriv a / a ^ 2"
   using fps_inverse_deriv[OF a0]
-  unfolding power2_eq_square fps_divide_def
-    fps_inverse_mult by simp
+  unfolding power2_eq_square fps_divide_def fps_inverse_mult
+  by simp
 
 lemma inverse_mult_eq_1': assumes f0: "f$0 \<noteq> (0::'a::field)"
   shows "f * inverse f= 1"
@@ -1090,7 +1151,8 @@
   assumes a0: "b$0 \<noteq> 0"
   shows "fps_deriv (a / b) = (fps_deriv a * b - a * fps_deriv b) / b ^ 2"
   using fps_inverse_deriv[OF a0]
-  by (simp add: fps_divide_def field_simps power2_eq_square fps_inverse_mult inverse_mult_eq_1'[OF a0])
+  by (simp add: fps_divide_def field_simps
+    power2_eq_square fps_inverse_mult inverse_mult_eq_1'[OF a0])
 
 
 lemma fps_inverse_gp': "inverse (Abs_fps(\<lambda>n. (1::'a::field)))
@@ -1136,7 +1198,8 @@
 definition fps_compose :: "('a::semiring_1) fps \<Rightarrow> 'a fps \<Rightarrow> 'a fps" (infixl "oo" 55) where
   fps_compose_def: "a oo b = Abs_fps (\<lambda>n. setsum (\<lambda>i. a$i * (b^i$n)) {0..n})"
 
-lemma fps_compose_nth: "(a oo b)$n = setsum (\<lambda>i. a$i * (b^i$n)) {0..n}" by (simp add: fps_compose_def)
+lemma fps_compose_nth: "(a oo b)$n = setsum (\<lambda>i. a$i * (b^i$n)) {0..n}"
+  by (simp add: fps_compose_def)
 
 lemma fps_compose_X[simp]: "a oo X = (a :: ('a :: comm_ring_1) fps)"
   by (simp add: fps_ext fps_compose_def mult_delta_right setsum_delta')
@@ -1207,7 +1270,7 @@
 
 lemma XDN_linear:
   "(XD ^^ n) (fps_const c * a + fps_const d * b) = fps_const c * (XD ^^ n) a + fps_const d * (XD ^^ n) (b :: ('a::comm_ring_1) fps)"
-  by (induct n, simp_all)
+  by (induct n) simp_all
 
 lemma fps_mult_X_deriv_shift: "X* fps_deriv a = Abs_fps (\<lambda>n. of_nat n* a$n)" by (simp add: fps_eq_iff)
 
@@ -1296,7 +1359,10 @@
       apply (clarsimp simp add: natpermute_def)
       unfolding xs' ys'
       using mn xs ys
-      unfolding natpermute_def by simp}
+      unfolding natpermute_def
+      apply simp
+      done
+  }
   moreover
   {fix l assume l: "l \<in> natpermute n k"
     let ?xs = "take h l"
@@ -1315,7 +1381,9 @@
       apply (rule exI[where x = "?ys"])
       using ls l 
       apply (auto simp add: natpermute_def l_take_drop simp del: append_take_drop_id)
-      by simp}
+      apply simp
+      done
+  }
   ultimately show ?thesis by blast
 qed
 
@@ -1324,7 +1392,8 @@
 lemma natpermute_0'[simp]: "natpermute 0 k = (if k = 0 then {[]} else {replicate k 0})"
   apply (auto simp add: set_replicate_conv_if natpermute_def)
   apply (rule nth_equalityI)
-  by simp_all
+  apply simp_all
+  done
 
 lemma natpermute_finite: "finite (natpermute n k)"
 proof(induct k arbitrary: n)
@@ -1368,7 +1437,8 @@
       unfolding nth_list_update[OF i'(1)]
       using i zxs
       by (case_tac "ia=i", auto simp del: replicate.simps)
-    then have "xs \<in> ?B" using i by blast}
+    then have "xs \<in> ?B" using i by blast
+  }
   moreover
   {fix i assume i: "i \<in> {0..k}"
     let ?xs = "replicate (k+1) 0 [i:=n]"
@@ -1383,7 +1453,8 @@
     finally
     have "?xs \<in> natpermute n (k+1)" using xsl unfolding natpermute_def mem_Collect_eq
       by blast
-    then have "?xs \<in> ?A"  using nxs  by blast}
+    then have "?xs \<in> ?A"  using nxs  by blast
+  }
   ultimately show ?thesis by auto
 qed
 
@@ -1409,7 +1480,8 @@
       unfolding fps_mult_nth H[rule_format, OF km] ..
     also have "\<dots> = (\<Sum>v\<in>natpermute n (m + 1). \<Prod>j\<in>{0..m}. a j $ v ! j)"
       apply (simp add: k)
-      unfolding natpermute_split[of m "m + 1", simplified, of n, unfolded natlist_trivial_1[unfolded One_nat_def] k]
+      unfolding natpermute_split[of m "m + 1", simplified, of n,
+        unfolded natlist_trivial_1[unfolded One_nat_def] k]
       apply (subst setsum_UN_disjoint)
       apply simp
       apply simp
@@ -1428,8 +1500,9 @@
       unfolding setprod_Un_disjoint[OF f0 d0, unfolded u0, unfolded k]
       apply (clarsimp simp add: natpermute_def nth_append)
       done
-    finally have "?P m n" .}
-  ultimately show "?P m n " by (cases m, auto)
+    finally have "?P m n" .
+  }
+  ultimately show "?P m n " by (cases m) auto
 qed
 
 text{* The special form for powers *}
@@ -1474,7 +1547,8 @@
         fix n assume H: "\<forall>m<n. b$m = c$m"
         {assume n0: "n=0"
           from h have "(b oo a)$n = (c oo a)$n" by simp
-          hence "b$n = c$n" using n0 by (simp add: fps_compose_nth)}
+          hence "b$n = c$n" using n0 by (simp add: fps_compose_nth)
+        }
         moreover
         {fix n1 assume n1: "n = Suc n1"
           have f: "finite {0 .. n1}" "finite {n}" by simp_all
@@ -1492,10 +1566,12 @@
             using startsby_zero_power_nth_same[OF a0]
             by simp
           from h[unfolded fps_eq_iff, rule_format, of n] th0 th1 a1
-          have "b$n = c$n" by auto}
-        ultimately show "b$n = c$n" by (cases n, auto)
+          have "b$n = c$n" by auto
+        }
+        ultimately show "b$n = c$n" by (cases n) auto
       qed}
-    then have ?rhs by (simp add: fps_eq_iff)}
+    then have ?rhs by (simp add: fps_eq_iff)
+  }
   ultimately show ?thesis by blast
 qed
 
@@ -1507,7 +1583,10 @@
   "radical r 0 a 0 = 1"
 | "radical r 0 a (Suc n) = 0"
 | "radical r (Suc k) a 0 = r (Suc k) (a$0)"
-| "radical r (Suc k) a (Suc n) = (a$ Suc n - setsum (\<lambda>xs. setprod (\<lambda>j. radical r (Suc k) a (xs ! j)) {0..k}) {xs. xs \<in> natpermute (Suc n) (Suc k) \<and> Suc n \<notin> set xs}) / (of_nat (Suc k) * (radical r (Suc k) a 0)^k)"
+| "radical r (Suc k) a (Suc n) =
+    (a$ Suc n - setsum (\<lambda>xs. setprod (\<lambda>j. radical r (Suc k) a (xs ! j)) {0..k})
+      {xs. xs \<in> natpermute (Suc n) (Suc k) \<and> Suc n \<notin> set xs}) /
+    (of_nat (Suc k) * (radical r (Suc k) a 0)^k)"
 by pat_completeness auto
 
 termination radical
@@ -1574,7 +1653,8 @@
   let ?K = "{0 ..k}"
   have fK: "finite ?K" by simp
   have fAK: "\<forall>i\<in>?K. finite (?A i)" by auto
-  have d: "\<forall>i\<in> ?K. \<forall>j\<in> ?K. i \<noteq> j \<longrightarrow> {replicate (k + 1) 0[i := n]} \<inter> {replicate (k + 1) 0[j := n]} = {}"
+  have d: "\<forall>i\<in> ?K. \<forall>j\<in> ?K. i \<noteq> j \<longrightarrow>
+    {replicate (k + 1) 0[i := n]} \<inter> {replicate (k + 1) 0[j := n]} = {}"
   proof(clarify)
     fix i j assume i: "i \<in> ?K" and j: "j\<in> ?K" and ij: "i\<noteq>j"
     {assume eq: "replicate (k+1) 0 [i:=n] = replicate (k+1) 0 [j:= n]"
@@ -1839,13 +1919,13 @@
 
 lemma radical_mult_distrib:
   fixes a:: "'a::field_char_0 fps"
-  assumes
-  k: "k > 0"
-  and ra0: "r k (a $ 0) ^ k = a $ 0"
-  and rb0: "r k (b $ 0) ^ k = b $ 0"
-  and a0: "a$0 \<noteq> 0"
-  and b0: "b$0 \<noteq> 0"
-  shows "r k ((a * b) $ 0) = r k (a $ 0) * r k (b $ 0) \<longleftrightarrow> fps_radical r (k) (a*b) = fps_radical r (k) a * fps_radical r (k) (b)"
+  assumes k: "k > 0"
+    and ra0: "r k (a $ 0) ^ k = a $ 0"
+    and rb0: "r k (b $ 0) ^ k = b $ 0"
+    and a0: "a$0 \<noteq> 0"
+    and b0: "b$0 \<noteq> 0"
+  shows "r k ((a * b) $ 0) = r k (a $ 0) * r k (b $ 0) \<longleftrightarrow>
+    fps_radical r (k) (a*b) = fps_radical r (k) a * fps_radical r (k) (b)"
 proof-
   {assume  r0': "r k ((a * b) $ 0) = r k (a $ 0) * r k (b $ 0)"
   from r0' have r0: "(r (k) ((a*b)$0)) ^ k = (a*b)$0"
@@ -2095,7 +2175,8 @@
 
 lemma fps_inv_ginv: "fps_inv = fps_ginv X"
   apply (auto simp add: fun_eq_iff fps_eq_iff fps_inv_def fps_ginv_def)
-  apply (induct_tac n rule: nat_less_induct, auto)
+  apply (induct_tac n rule: nat_less_induct)
+  apply auto
   apply (case_tac na)
   apply simp
   apply simp
@@ -2305,7 +2386,7 @@
 qed
 
 lemma fps_const_power[simp]: "fps_const (c::'a::ring_1) ^ n = fps_const (c^n)"
-by (induct n, auto)
+  by (induct n) auto
 
 lemma fps_compose_radical:
   assumes b0: "b$0 = (0::'a::field_char_0)"
@@ -2532,7 +2613,7 @@
 qed
 
 lemma E_nth_deriv[simp]: "fps_nth_deriv n (E (a::'a::field_char_0)) = (fps_const a)^n * (E a)"
-  by (induct n, auto simp add: power_Suc)
+  by (induct n) (auto simp add: power_Suc)
 
 lemma X_compose_E[simp]: "X oo E (a::'a::{field}) = E a - 1"
   by (simp add: fps_eq_iff X_fps_compose)
@@ -2565,7 +2646,7 @@
 qed
 
 lemma E_power_mult: "(E (c::'a::field_char_0))^n = E (of_nat n * c)"
-  by (induct n, auto simp add: field_simps E_add_mult power_Suc)
+  by (induct n) (auto simp add: field_simps E_add_mult power_Suc)
 
 lemma radical_E:
   assumes r: "r (Suc k) 1 = 1" 
@@ -3197,10 +3278,10 @@
 
 lemma foldl_mult_start:
   "foldl (%r x. r * f x) (v::'a::comm_ring_1) as * x = foldl (%r x. r * f x) (v * x) as "
-  by (induct as arbitrary: x v, auto simp add: algebra_simps)
+  by (induct as arbitrary: x v) (auto simp add: algebra_simps)
 
 lemma foldr_mult_foldl: "foldr (%x r. r * f x) as v = foldl (%r x. r * f x) (v :: 'a::comm_ring_1) as"
-  by (induct as arbitrary: v, auto simp add: foldl_mult_start)
+  by (induct as arbitrary: v) (auto simp add: foldl_mult_start)
 
 lemma F_nth_alt: "F as bs c $ n = foldr (\<lambda>a r. r * pochhammer a n) as (c ^ n) /
     foldr (\<lambda>b r. r * pochhammer b n) bs (of_nat (fact n))"
@@ -3224,11 +3305,12 @@
   apply simp
   apply (subgoal_tac "ALL as. foldl (%(r::'a) (a::'a). r) 1 as = 1")
   apply auto
-  apply (induct_tac as, auto)
+  apply (induct_tac as)
+  apply auto
   done
 
 lemma foldl_prod_prod: "foldl (%(r::'b::comm_ring_1) (x::'a::comm_ring_1). r * f x) v as * foldl (%r x. r * g x) w as = foldl (%r x. r * f x * g x) (v*w) as"
-  by (induct as arbitrary: v w, auto simp add: algebra_simps)
+  by (induct as arbitrary: v w) (auto simp add: algebra_simps)
 
 
 lemma F_rec: "F as bs c $ Suc n = ((foldl (%r a. r* (a + of_nat n)) c as)/ (foldl (%r b. r * (b + of_nat n)) (of_nat (Suc n)) bs )) * F as bs c $ n"
@@ -3276,7 +3358,7 @@
 
 lemma XDp_foldr_nth[simp]: "foldr (%c r. XDp c o r) cs (%c. XDp c a) c0 $ n = 
   foldr (%c r. (c + of_nat n) * r) cs (c0 + of_nat n) * a$n"
-  by (induct cs arbitrary: c0, auto simp add: algebra_simps)
+  by (induct cs arbitrary: c0) (auto simp add: algebra_simps)
 
 lemma genric_XDp_foldr_nth:
   assumes 
@@ -3284,6 +3366,6 @@
 
   shows "foldr (%c r. f c o r) cs (%c. g c a) c0 $ n = 
   foldr (%c r. (k c + of_nat n) * r) cs (g c0 a $ n)"
-  by (induct cs arbitrary: c0, auto simp add: algebra_simps f)
+  by (induct cs arbitrary: c0) (auto simp add: algebra_simps f)
 
 end
diff -r ff570720ba1c -r 4218d7b5d892 src/HOL/Library/Order_Relation.thy
--- a/src/HOL/Library/Order_Relation.thy	Fri Aug 10 17:17:05 2012 +0200
+++ b/src/HOL/Library/Order_Relation.thy	Fri Aug 10 18:03:46 2012 +0200
@@ -71,9 +71,9 @@
 lemma subset_Image_Image_iff:
   "\<lbrakk> Preorder r; A \<subseteq> Field r; B \<subseteq> Field r\<rbrakk> \<Longrightarrow>
    r `` A \<subseteq> r `` B \<longleftrightarrow> (\<forall>a\<in>A.\<exists>b\<in>B. (b,a):r)"
-apply(auto simp add: subset_eq preorder_on_def refl_on_def Image_def)
-apply metis
-by(metis trans_def)
+unfolding preorder_on_def refl_on_def Image_def
+apply (simp add: subset_eq)
+unfolding trans_def by fast
 
 lemma subset_Image1_Image1_iff:
   "\<lbrakk> Preorder r; a : Field r; b : Field r\<rbrakk> \<Longrightarrow> r `` {a} \<subseteq> r `` {b} \<longleftrightarrow> (b,a):r"
diff -r ff570720ba1c -r 4218d7b5d892 src/HOL/Library/Zorn.thy
--- a/src/HOL/Library/Zorn.thy	Fri Aug 10 17:17:05 2012 +0200
+++ b/src/HOL/Library/Zorn.thy	Fri Aug 10 18:03:46 2012 +0200
@@ -8,7 +8,7 @@
 header {* Zorn's Lemma *}
 
 theory Zorn
-imports Order_Relation Main
+imports Order_Relation
 begin
 
 (* Define globally? In Set.thy? *)
@@ -143,7 +143,7 @@
  the subset relation!*}
 
 lemma empty_set_mem_chain: "({} :: 'a set set) \<in> chain S"
-by (unfold chain_def chain_subset_def) auto
+  by (unfold chain_def chain_subset_def) simp
 
 lemma super_subset_chain: "super S c \<subseteq> chain S"
   by (unfold super_def) blast
@@ -152,13 +152,13 @@
   by (unfold maxchain_def) blast
 
 lemma mem_super_Ex: "c \<in> chain S - maxchain S ==> EX d. d \<in> super S c"
-  by (unfold super_def maxchain_def) auto
+  by (unfold super_def maxchain_def) simp
 
 lemma select_super:
      "c \<in> chain S - maxchain S ==> (\<some>c'. c': super S c): super S c"
   apply (erule mem_super_Ex [THEN exE])
   apply (rule someI2)
-  apply auto
+  apply simp+
   done
 
 lemma select_not_equals:
@@ -286,7 +286,7 @@
     proof (simp add:Chain_def, intro allI impI, elim conjE)
       fix a b
       assume "a \<in> Field r" "?B a \<in> C" "b \<in> Field r" "?B b \<in> C"
-      hence "?B a \<subseteq> ?B b \<or> ?B b \<subseteq> ?B a" using 2 by auto
+      hence "?B a \<subseteq> ?B b \<or> ?B b \<subseteq> ?B a" using 2 by simp
       thus "(a, b) \<in> r \<or> (b, a) \<in> r" using `Preorder r` `a:Field r` `b:Field r`
         by (simp add:subset_Image1_Image1_iff)
     qed
@@ -296,7 +296,7 @@
       fix a B assume aB: "B:C" "a:B"
       with 1 obtain x where "x:Field r" "B = r^-1 `` {x}" by auto
       thus "(a,u) : r" using uA aB `Preorder r`
-        by (auto simp add: preorder_on_def refl_on_def) (metis transD)
+        by (simp add: preorder_on_def refl_on_def) (rule transD, blast+)
     qed
     thus "EX u:Field r. ?P u" using `u:Field r` by blast
   qed
@@ -326,8 +326,7 @@
 
 lemma trans_init_seg_of:
   "r initial_segment_of s \<Longrightarrow> s initial_segment_of t \<Longrightarrow> r initial_segment_of t"
-by(simp (no_asm_use) add: init_seg_of_def)
-  (metis Domain_iff UnCI Un_absorb2 subset_trans)
+by (simp (no_asm_use) add: init_seg_of_def) (metis (no_types) in_mono order_trans)
 
 lemma antisym_init_seg_of:
   "r initial_segment_of s \<Longrightarrow> s initial_segment_of r \<Longrightarrow> r=s"
@@ -335,20 +334,17 @@
 
 lemma Chain_init_seg_of_Union:
   "R \<in> Chain init_seg_of \<Longrightarrow> r\<in>R \<Longrightarrow> r initial_segment_of \<Union>R"
-by(auto simp add:init_seg_of_def Chain_def Ball_def) blast
+by(simp add: init_seg_of_def Chain_def Ball_def) blast
 
 lemma chain_subset_trans_Union:
   "chain\<^bsub>\<subseteq>\<^esub> R \<Longrightarrow> \<forall>r\<in>R. trans r \<Longrightarrow> trans(\<Union>R)"
-apply(auto simp add:chain_subset_def)
+apply(simp add:chain_subset_def)
 apply(simp (no_asm_use) add:trans_def)
-apply (metis subsetD)
-done
+by (metis subsetD)
 
 lemma chain_subset_antisym_Union:
   "chain\<^bsub>\<subseteq>\<^esub> R \<Longrightarrow> \<forall>r\<in>R. antisym r \<Longrightarrow> antisym(\<Union>R)"
-apply(auto simp add:chain_subset_def antisym_def)
-apply (metis subsetD)
-done
+by (simp add:chain_subset_def antisym_def) (metis subsetD)
 
 lemma chain_subset_Total_Union:
 assumes "chain\<^bsub>\<subseteq>\<^esub> R" "\<forall>r\<in>R. Total r"
@@ -403,7 +399,7 @@
 -- {*The initial segment relation on well-orders: *}
   let ?WO = "{r::('a*'a)set. Well_order r}"
   def I \<equiv> "init_seg_of \<inter> ?WO \<times> ?WO"
-  have I_init: "I \<subseteq> init_seg_of" by(auto simp:I_def)
+  have I_init: "I \<subseteq> init_seg_of" by(simp add: I_def)
   hence subch: "!!R. R : Chain I \<Longrightarrow> chain\<^bsub>\<subseteq>\<^esub> R"
     by(auto simp:init_seg_of_def chain_subset_def Chain_def)
   have Chain_wo: "!!R r. R \<in> Chain I \<Longrightarrow> r \<in> R \<Longrightarrow> Well_order r"
@@ -437,7 +433,7 @@
       by(simp add: Chain_init_seg_of_Union)
     ultimately have "\<Union>R : ?WO \<and> (\<forall>r\<in>R. (r,\<Union>R) : I)"
       using mono_Chain[OF I_init] `R \<in> Chain I`
-      by(simp (no_asm) add:I_def del:Field_Union)(metis Chain_wo subsetD)
+      by(simp (no_asm) add:I_def del:Field_Union)(metis Chain_wo)
   }
   hence 1: "\<forall>R \<in> Chain I. \<exists>u\<in>Field I. \<forall>r\<in>R. (r,u) : I" by (subst FI) blast
 --{*Zorn's Lemma yields a maximal well-order m:*}
@@ -475,7 +471,7 @@
     moreover have "wf(?m-Id)"
     proof-
       have "wf ?s" using `x \<notin> Field m`
-        by(auto simp add:wf_eq_minimal Field_def Domain_unfold Domain_converse [symmetric]) metis
+        by(simp add:wf_eq_minimal Field_def Domain_unfold Domain_converse [symmetric]) metis
       thus ?thesis using `wf(m-Id)` `x \<notin> Field m`
         wf_subset[OF `wf ?s` Diff_subset]
         by (fastforce intro!: wf_Un simp add: Un_Diff Field_def)
diff -r ff570720ba1c -r 4218d7b5d892 src/Pure/General/linear_set.scala
--- a/src/Pure/General/linear_set.scala	Fri Aug 10 17:17:05 2012 +0200
+++ b/src/Pure/General/linear_set.scala	Fri Aug 10 18:03:46 2012 +0200
@@ -34,8 +34,6 @@
 {
   override def companion: GenericCompanion[Linear_Set] = Linear_Set
 
-  def reverse: Linear_Set[A] = new Linear_Set(end, start, prevs, nexts)
-
 
   /* relative addressing */
 
@@ -76,7 +74,7 @@
             }
       }
 
-  def append_after(hook: Option[A], elems: Seq[A]): Linear_Set[A] =
+  def append_after(hook: Option[A], elems: Seq[A]): Linear_Set[A] =  // FIXME reverse fold
     ((hook, this) /: elems) {
       case ((last, set), elem) => (Some(elem), set.insert_after(last, elem))
     }._2
@@ -147,6 +145,10 @@
         case Some(stop) => iterator(from).takeWhile(_ != stop)
       }
 
+  def reverse: Linear_Set[A] = new Linear_Set(end, start, prevs, nexts)
+
+  override def last: A = reverse.head
+
   def + (elem: A): Linear_Set[A] = insert_after(end, elem)
 
   def - (elem: A): Linear_Set[A] =
diff -r ff570720ba1c -r 4218d7b5d892 src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Fri Aug 10 17:17:05 2012 +0200
+++ b/src/Pure/General/scan.scala	Fri Aug 10 18:03:46 2012 +0200
@@ -375,9 +375,9 @@
 
       val recover_delimited =
         (quoted_prefix("\"") | (quoted_prefix("`") | (verbatim_prefix | comment_prefix))) ^^
-          (x => Token(Token.Kind.UNPARSED, x))
+          (x => Token(Token.Kind.ERROR, x))
 
-      val bad = one(_ => true) ^^ (x => Token(Token.Kind.UNPARSED, x))
+      val bad = one(_ => true) ^^ (x => Token(Token.Kind.ERROR, x))
 
       space | (recover_delimited |
         (((ident | (var_ | (type_ident | (type_var | (float | (nat_ | sym_ident)))))) |||
diff -r ff570720ba1c -r 4218d7b5d892 src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Fri Aug 10 17:17:05 2012 +0200
+++ b/src/Pure/Isar/token.scala	Fri Aug 10 18:03:46 2012 +0200
@@ -28,6 +28,7 @@
     val VERBATIM = Value("verbatim text")
     val SPACE = Value("white space")
     val COMMENT = Value("comment text")
+    val ERROR = Value("bad input")
     val UNPARSED = Value("unparsed input")
   }
 
@@ -89,8 +90,15 @@
   def is_space: Boolean = kind == Token.Kind.SPACE
   def is_comment: Boolean = kind == Token.Kind.COMMENT
   def is_proper: Boolean = !is_space && !is_comment
+  def is_error: Boolean = kind == Token.Kind.ERROR
   def is_unparsed: Boolean = kind == Token.Kind.UNPARSED
 
+  def is_unfinished: Boolean = is_error &&
+   (source.startsWith("\"") ||
+    source.startsWith("`") ||
+    source.startsWith("{*") ||
+    source.startsWith("(*"))
+
   def is_begin: Boolean = is_keyword && source == "begin"
   def is_end: Boolean = is_keyword && source == "end"
 
diff -r ff570720ba1c -r 4218d7b5d892 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Fri Aug 10 17:17:05 2012 +0200
+++ b/src/Pure/ML/ml_lex.ML	Fri Aug 10 18:03:46 2012 +0200
@@ -115,7 +115,7 @@
   | String    => Isabelle_Markup.ML_string
   | Space     => Markup.empty
   | Comment   => Isabelle_Markup.ML_comment
-  | Error _   => Isabelle_Markup.ML_malformed
+  | Error msg => Isabelle_Markup.bad msg
   | EOF       => Markup.empty;
 
 fun token_markup kind x =
diff -r ff570720ba1c -r 4218d7b5d892 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Fri Aug 10 17:17:05 2012 +0200
+++ b/src/Pure/PIDE/command.scala	Fri Aug 10 18:03:46 2012 +0200
@@ -111,8 +111,8 @@
     {
       val cmds1 = this.commands
       val cmds2 = that.commands
-      require(cmds1.forall(_.is_defined))
-      require(cmds2.forall(_.is_defined))
+      require(!cmds1.exists(_.is_undefined))
+      require(!cmds2.exists(_.is_undefined))
       cmds1.length == cmds2.length &&
         (cmds1.iterator zip cmds2.iterator).forall({ case (c1, c2) => c1.id == c2.id })
     }
@@ -128,10 +128,12 @@
 {
   /* classification */
 
-  def is_defined: Boolean = id != Document.no_id
+  def is_undefined: Boolean = id == Document.no_id
+  val is_unparsed: Boolean = span.exists(_.is_unparsed)
+  val is_unfinished: Boolean = span.exists(_.is_unfinished)
 
   val is_ignored: Boolean = !span.exists(_.is_proper)
-  val is_malformed: Boolean = !is_ignored && (!span.head.is_command || span.exists(_.is_unparsed))
+  val is_malformed: Boolean = !is_ignored && (!span.head.is_command || span.exists(_.is_error))
   def is_command: Boolean = !is_ignored && !is_malformed
 
   def name: String =
diff -r ff570720ba1c -r 4218d7b5d892 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Fri Aug 10 17:17:05 2012 +0200
+++ b/src/Pure/PIDE/document.ML	Fri Aug 10 18:03:46 2012 +0200
@@ -17,7 +17,7 @@
   val print_id: id -> string
   type node_header = string * Thy_Header.header * string list
   datatype node_edit =
-    Clear |
+    Clear |    (* FIXME unused !? *)
     Edits of (command_id option * command_id option) list |
     Deps of node_header |
     Perspective of command_id list
diff -r ff570720ba1c -r 4218d7b5d892 src/Pure/PIDE/isabelle_markup.ML
--- a/src/Pure/PIDE/isabelle_markup.ML	Fri Aug 10 17:17:05 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.ML	Fri Aug 10 18:03:46 2012 +0200
@@ -55,7 +55,6 @@
   val ML_charN: string val ML_char: Markup.T
   val ML_stringN: string val ML_string: Markup.T
   val ML_commentN: string val ML_comment: Markup.T
-  val ML_malformedN: string val ML_malformed: Markup.T
   val ML_defN: string
   val ML_openN: string
   val ML_structN: string
@@ -74,11 +73,7 @@
   val verbatimN: string val verbatim: Markup.T
   val commentN: string val comment: Markup.T
   val controlN: string val control: Markup.T
-  val malformedN: string val malformed: Markup.T
   val tokenN: string val token: Properties.T -> Markup.T
-  val command_spanN: string val command_span: string -> Markup.T
-  val ignored_spanN: string val ignored_span: Markup.T
-  val malformed_spanN: string val malformed_span: Markup.T
   val elapsedN: string
   val cpuN: string
   val gcN: string
@@ -100,7 +95,8 @@
   val promptN: string val prompt: Markup.T
   val reportN: string val report: Markup.T
   val no_reportN: string val no_report: Markup.T
-  val badN: string val bad: Markup.T
+  val messageN: string
+  val badN: string val bad: string -> Markup.T
   val functionN: string
   val assign_execs: Properties.T
   val removed_versions: Properties.T
@@ -211,7 +207,6 @@
 val (ML_charN, ML_char) = markup_elem "ML_char";
 val (ML_stringN, ML_string) = markup_elem "ML_string";
 val (ML_commentN, ML_comment) = markup_elem "ML_comment";
-val (ML_malformedN, ML_malformed) = markup_elem "ML_malformed";
 
 val ML_defN = "ML_def";
 val ML_openN = "ML_open";
@@ -240,15 +235,10 @@
 val (verbatimN, verbatim) = markup_elem "verbatim";
 val (commentN, comment) = markup_elem "comment";
 val (controlN, control) = markup_elem "control";
-val (malformedN, malformed) = markup_elem "malformed";
 
 val tokenN = "token";
 fun token props = (tokenN, props);
 
-val (command_spanN, command_span) = markup_string "command_span" Markup.nameN;
-val (ignored_spanN, ignored_span) = markup_elem "ignored_span";
-val (malformed_spanN, malformed_span) = markup_elem "malformed_span";
-
 
 (* timing *)
 
@@ -297,7 +287,11 @@
 val (reportN, report) = markup_elem "report";
 val (no_reportN, no_report) = markup_elem "no_report";
 
-val (badN, bad) = markup_elem "bad";
+val messageN = "message"
+val badN = "bad"
+
+fun bad "" = (badN, [])
+  | bad msg = (badN, [(messageN, msg)]);
 
 
 (* protocol message functions *)
diff -r ff570720ba1c -r 4218d7b5d892 src/Pure/PIDE/isabelle_markup.scala
--- a/src/Pure/PIDE/isabelle_markup.scala	Fri Aug 10 17:17:05 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.scala	Fri Aug 10 18:03:46 2012 +0200
@@ -132,7 +132,6 @@
   val ML_CHAR = "ML_char"
   val ML_STRING = "ML_string"
   val ML_COMMENT = "ML_comment"
-  val ML_MALFORMED = "ML_malformed"
 
   val ML_DEF = "ML_def"
   val ML_OPEN = "ML_open"
@@ -150,11 +149,6 @@
   val VERBATIM = "verbatim"
   val COMMENT = "comment"
   val CONTROL = "control"
-  val MALFORMED = "malformed"
-
-  val COMMAND_SPAN = "command_span"
-  val IGNORED_SPAN = "ignored_span"
-  val MALFORMED_SPAN = "malformed_span"
 
 
   /* timing */
@@ -242,6 +236,7 @@
 
   val NO_REPORT = "no_report"
 
+  val Message = new Properties.String("message")
   val BAD = "bad"
 
 
diff -r ff570720ba1c -r 4218d7b5d892 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Fri Aug 10 17:17:05 2012 +0200
+++ b/src/Pure/PIDE/protocol.ML	Fri Aug 10 18:03:46 2012 +0200
@@ -33,7 +33,7 @@
             let open XML.Decode in
               list (pair string
                 (variant
-                 [fn ([], []) => Document.Clear,
+                 [fn ([], []) => Document.Clear,  (* FIXME unused !? *)
                   fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
                   fn ([], a) =>
                     let
diff -r ff570720ba1c -r 4218d7b5d892 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Fri Aug 10 17:17:05 2012 +0200
+++ b/src/Pure/PIDE/protocol.scala	Fri Aug 10 18:03:46 2012 +0200
@@ -213,7 +213,7 @@
       def encode_edit(name: Document.Node.Name)
           : T[Document.Node.Edit[(Option[Command], Option[Command]), Command.Perspective]] =
         variant(List(
-          { case Document.Node.Clear() => (Nil, Nil) },
+          { case Document.Node.Clear() => (Nil, Nil) },  // FIXME unused !?
           { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
           { case Document.Node.Deps(header) =>
               val dir = Isabelle_System.posix_path(name.dir)
diff -r ff570720ba1c -r 4218d7b5d892 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Fri Aug 10 17:17:05 2012 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Fri Aug 10 18:03:46 2012 +0200
@@ -318,7 +318,7 @@
 fun parse_failed ctxt pos msg kind =
   cat_error msg ("Failed to parse " ^ kind ^
     Markup.markup Isabelle_Markup.report
-      (Context_Position.reported_text ctxt pos Isabelle_Markup.bad ""));
+      (Context_Position.reported_text ctxt pos (Isabelle_Markup.bad "") ""));
 
 fun parse_sort ctxt =
   Syntax.parse_token ctxt Term_XML.Decode.sort Isabelle_Markup.sort
@@ -609,7 +609,7 @@
       | token_trans "_tvar" x = SOME (Pretty.mark_str (Isabelle_Markup.tvar, x))
       | token_trans "_free" x = SOME (Pretty.marks_str (free_or_skolem ctxt x))
       | token_trans "_bound" x = SOME (Pretty.mark_str (Isabelle_Markup.bound, x))
-      | token_trans "_loose" x = SOME (Pretty.mark_str (Isabelle_Markup.malformed, x))
+      | token_trans "_loose" x = SOME (Pretty.mark_str (Isabelle_Markup.bad "", x))
       | token_trans "_var" x = SOME (Pretty.mark_str (var_or_skolem x))
       | token_trans "_numeral" x = SOME (Pretty.mark_str (Isabelle_Markup.numeral, x))
       | token_trans "_inner_string" x = SOME (Pretty.mark_str (Isabelle_Markup.inner_string, x))
diff -r ff570720ba1c -r 4218d7b5d892 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Fri Aug 10 17:17:05 2012 +0200
+++ b/src/Pure/System/session.scala	Fri Aug 10 18:03:46 2012 +0200
@@ -453,7 +453,7 @@
     header: Document.Node.Header, perspective: Text.Perspective, text: String)
   {
     edit(List(header_edit(name, header),
-      name -> Document.Node.Clear(),    // FIXME diff wrt. existing node
+      name -> Document.Node.Clear(),
       name -> Document.Node.Edits(List(Text.Edit.insert(0, text))),
       name -> Document.Node.Perspective(perspective)))
   }
diff -r ff570720ba1c -r 4218d7b5d892 src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Fri Aug 10 17:17:05 2012 +0200
+++ b/src/Pure/Thy/thy_syntax.ML	Fri Aug 10 18:03:46 2012 +0200
@@ -54,7 +54,7 @@
   | Token.Space         => Markup.empty
   | Token.Comment       => Isabelle_Markup.comment
   | Token.InternalValue => Markup.empty
-  | Token.Error _       => Isabelle_Markup.malformed
+  | Token.Error msg     => Isabelle_Markup.bad msg
   | Token.Sync          => Isabelle_Markup.control
   | Token.EOF           => Isabelle_Markup.control;
 
@@ -74,7 +74,8 @@
     val malformed_symbols =
       Symbol_Pos.explode (Token.source_position_of tok)
       |> map_filter (fn (sym, pos) =>
-          if Symbol.is_malformed sym then SOME (pos, Isabelle_Markup.malformed) else NONE);
+          if Symbol.is_malformed sym
+          then SOME (pos, Isabelle_Markup.bad "Malformed symbol") else NONE);
     val is_malformed = Token.is_error tok orelse not (null malformed_symbols);
     val reports = (Token.position_of tok, token_markup tok) :: malformed_symbols;
   in (is_malformed, reports) end;
@@ -127,18 +128,7 @@
 
 (* present *)
 
-local
-
-fun kind_markup (Command name) = Isabelle_Markup.command_span name
-  | kind_markup Ignored = Isabelle_Markup.ignored_span
-  | kind_markup Malformed = Isabelle_Markup.malformed_span;
-
-in
-
-fun present_span span =
-  Markup.enclose (kind_markup (span_kind span)) (implode (map present_token (span_content span)));
-
-end;
+val present_span = implode o map present_token o span_content;
 
 
 
diff -r ff570720ba1c -r 4218d7b5d892 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Fri Aug 10 17:17:05 2012 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Fri Aug 10 18:03:46 2012 +0200
@@ -165,7 +165,7 @@
 
   /** text edits **/
 
-  /* phase 1: edit individual command source */
+  /* edit individual command source */
 
   @tailrec private def edit_text(eds: List[Text.Edit], commands: Linear_Set[Command])
       : Linear_Set[Command] =
@@ -194,7 +194,7 @@
   }
 
 
-  /* phase 2: recover command spans */
+  /* reparse range of command spans */
 
   @tailrec private def chop_common(
       cmds: List[Command], spans: List[Command.Span]): (List[Command], List[Command.Span]) =
@@ -203,69 +203,118 @@
       case _ => (cmds, spans)
     }
 
-  private def trim_common(
-      cmds: List[Command], spans: List[Command.Span]): (List[Command], List[Command.Span]) =
+  private def reparse_spans(
+    syntax: Outer_Syntax,
+    name: Document.Node.Name,
+    commands: Linear_Set[Command],
+    first: Command, last: Command): Linear_Set[Command] =
   {
-    val (cmds1, spans1) = chop_common(cmds, spans)
+    val cmds0 = commands.iterator(first, last).toList
+    val spans0 = parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString))
+
+    val (cmds1, spans1) = chop_common(cmds0, spans0)
+
     val (rev_cmds2, rev_spans2) = chop_common(cmds1.reverse, spans1.reverse)
-    (rev_cmds2.reverse, rev_spans2.reverse)
+    val cmds2 = rev_cmds2.reverse
+    val spans2 = rev_spans2.reverse
+
+    cmds2 match {
+      case Nil =>
+        assert(spans2.isEmpty)
+        commands
+      case cmd :: _ =>
+        val hook = commands.prev(cmd)
+        val inserted = spans2.map(span => Command(Document.new_id(), name, span))
+        (commands /: cmds2)(_ - _).append_after(hook, inserted)
+    }
   }
 
+
+  /* recover command spans after edits */
+
+  // FIXME somewhat slow
   private def recover_spans(
     syntax: Outer_Syntax,
-    node_name: Document.Node.Name,
+    name: Document.Node.Name,
     perspective: Command.Perspective,
-    old_commands: Linear_Set[Command]): Linear_Set[Command] =
+    commands: Linear_Set[Command]): Linear_Set[Command] =
   {
-    val visible = perspective.commands.iterator.filter(_.is_defined).toSet
+    val visible = perspective.commands.toSet
 
-    def next_invisible_command(commands: Linear_Set[Command], from: Command): Command =
-      commands.iterator(from).dropWhile(cmd => !cmd.is_command || visible(cmd))
-        .find(_.is_command) getOrElse commands.last
-
-    @tailrec def recover(commands: Linear_Set[Command]): Linear_Set[Command] =
-      commands.iterator.find(cmd => !cmd.is_defined) match {
-        case Some(first_undefined) =>
-          val first = next_invisible_command(commands.reverse, first_undefined)
-          val last = next_invisible_command(commands, first_undefined)
+    def next_invisible_command(cmds: Linear_Set[Command], from: Command): Command =
+      cmds.iterator(from).dropWhile(cmd => !cmd.is_command || visible(cmd))
+        .find(_.is_command) getOrElse cmds.last
 
-          val cmds0 = commands.iterator(first, last).toList
-          val spans0 = parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString))
-
-          val (cmds, spans) = trim_common(cmds0, spans0)
-          val new_commands =
-            cmds match {
-              case Nil =>
-                assert(spans.isEmpty)
-                commands
-              case cmd :: _ =>
-                val hook = commands.prev(cmd)
-                val inserted = spans.map(span => Command(Document.new_id(), node_name, span))
-                (commands /: cmds)(_ - _).append_after(hook, inserted)
-            }
-          recover(new_commands)
-
-        case None => commands
+    @tailrec def recover(cmds: Linear_Set[Command]): Linear_Set[Command] =
+      cmds.find(_.is_unparsed) match {
+        case Some(first_unparsed) =>
+          val first = next_invisible_command(cmds.reverse, first_unparsed)
+          val last = next_invisible_command(cmds, first_unparsed)
+          recover(reparse_spans(syntax, name, cmds, first, last))
+        case None => cmds
       }
-    recover(old_commands)
+    recover(commands)
   }
 
 
-  /* phase 3: full reparsing after syntax change */
+  /* consolidate unfinished spans */
 
-  private def reparse_spans(
+  private def consolidate_spans(
     syntax: Outer_Syntax,
-    node_name: Document.Node.Name,
+    name: Document.Node.Name,
+    perspective: Command.Perspective,
     commands: Linear_Set[Command]): Linear_Set[Command] =
   {
-    val cmds = commands.toList
-    val spans1 = parse_spans(syntax.scan(cmds.map(_.source).mkString))
-    if (cmds.map(_.span) == spans1) commands
-    else Linear_Set(spans1.map(span => Command(Document.new_id(), node_name, span)): _*)
+    if (perspective.commands.isEmpty) commands
+    else {
+      commands.find(_.is_unfinished) match {
+        case Some(first_unfinished) =>
+          val visible = perspective.commands.toSet
+          commands.reverse.find(visible) match {
+            case Some(last_visible) =>
+              reparse_spans(syntax, name, commands, first_unfinished, last_visible)
+            case None => commands
+          }
+        case None => commands
+      }
+    }
   }
 
 
-  /* main phase */
+  /* main */
+
+  private def diff_commands(old_cmds: Linear_Set[Command], new_cmds: Linear_Set[Command])
+    : List[(Option[Command], Option[Command])] =
+  {
+    val removed = old_cmds.iterator.filter(!new_cmds.contains(_)).toList
+    val inserted = new_cmds.iterator.filter(!old_cmds.contains(_)).toList
+
+    removed.reverse.map(cmd => (old_cmds.prev(cmd), None)) :::
+    inserted.map(cmd => (new_cmds.prev(cmd), Some(cmd)))
+  }
+
+  private def text_edit(syntax: Outer_Syntax,
+    node: Document.Node, edit: Document.Edit_Text): Document.Node =
+  {
+    edit match {
+      case (_, Document.Node.Clear()) => node.clear
+
+      case (name, Document.Node.Edits(text_edits)) =>
+        val commands0 = node.commands
+        val commands1 = edit_text(text_edits, commands0)
+        val commands2 = recover_spans(syntax, name, node.perspective, commands1)
+        node.update_commands(commands2)
+
+      case (_, Document.Node.Deps(_)) => node
+
+      case (name, Document.Node.Perspective(text_perspective)) =>
+        val perspective = command_perspective(node, text_perspective)
+        if (node.perspective same perspective) node
+        else
+          node.update_perspective(perspective)
+            .update_commands(consolidate_spans(syntax, name, perspective, node.commands))
+    }
+  }
 
   def text_edits(
       base_syntax: Outer_Syntax,
@@ -279,40 +328,29 @@
     var nodes = nodes0
     val doc_edits = new mutable.ListBuffer[Document.Edit_Command]; doc_edits ++= doc_edits0
 
-    (edits ::: reparse.map((_, Document.Node.Edits(Nil)))) foreach {
-      case (name, Document.Node.Clear()) =>
-        doc_edits += (name -> Document.Node.Clear())
-        nodes += (name -> nodes(name).clear)
+    val node_edits =
+      (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1)
+        .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]]  // FIXME ???
 
-      case (name, Document.Node.Edits(text_edits)) =>
+    node_edits foreach {
+      case (name, edits) =>
         val node = nodes(name)
-        val commands0 = node.commands
-        val commands1 = edit_text(text_edits, commands0)
-        val commands2 = recover_spans(syntax, name, node.perspective, commands1)   // FIXME somewhat slow
-        val commands3 =
-          if (reparse_set.contains(name)) reparse_spans(syntax, name, commands2)  // slow
-          else commands2
-
-        val removed_commands = commands0.iterator.filter(!commands3.contains(_)).toList
-        val inserted_commands = commands3.iterator.filter(!commands0.contains(_)).toList
+        val commands = node.commands
 
-        val cmd_edits =
-          removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
-          inserted_commands.map(cmd => (commands3.prev(cmd), Some(cmd)))
-
-        doc_edits += (name -> Document.Node.Edits(cmd_edits))
-        nodes += (name -> node.update_commands(commands3))
-
-      case (name, Document.Node.Deps(_)) =>
+        val node1 =
+          if (reparse_set(name) && !commands.isEmpty)
+            node.update_commands(reparse_spans(syntax, name, commands, commands.head, commands.last))
+          else node
+        val node2 = (node1 /: edits)(text_edit(syntax, _, _))
 
-      case (name, Document.Node.Perspective(text_perspective)) =>
-        val node = nodes(name)
-        val perspective = command_perspective(node, text_perspective)
-        if (!(node.perspective same perspective)) {
-          doc_edits += (name -> Document.Node.Perspective(perspective))
-          nodes += (name -> node.update_perspective(perspective))
-        }
+        if (!(node.perspective same node2.perspective))
+          doc_edits += (name -> Document.Node.Perspective(node2.perspective))
+
+        doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands)))
+
+        nodes += (name -> node2)
     }
+
     (doc_edits.toList, Document.Version.make(syntax, nodes))
   }
 }
diff -r ff570720ba1c -r 4218d7b5d892 src/Tools/jEdit/src/isabelle_rendering.scala
--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Fri Aug 10 17:17:05 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Fri Aug 10 18:03:46 2012 +0200
@@ -22,7 +22,7 @@
 {
   /* physical rendering */
 
-  // see http://www.w3schools.com/css/css_colornames.asp
+  // see http://www.w3schools.com/cssref/css_colornames.asp
 
   def get_color(s: String): Color = ColorFactory.getInstance.getColor(s)
 
@@ -104,18 +104,25 @@
   }
 
 
+  private def tooltip_text(msg: XML.Body): String =
+    Pretty.string_of(msg, margin = Isabelle.Int_Property("tooltip-margin"))
+
   def tooltip_message(snapshot: Document.Snapshot, range: Text.Range): Option[String] =
   {
     val msgs =
       snapshot.cumulate_markup[SortedMap[Long, String]](range, SortedMap.empty,
-        Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
+        Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR,
+          Isabelle_Markup.BAD)),
         {
-          case (msgs, Text.Info(_, msg @ XML.Elem(Markup(markup, Isabelle_Markup.Serial(serial)), _)))
+          case (msgs, Text.Info(_, msg @
+              XML.Elem(Markup(markup, Isabelle_Markup.Serial(serial)), _)))
           if markup == Isabelle_Markup.WRITELN ||
               markup == Isabelle_Markup.WARNING ||
               markup == Isabelle_Markup.ERROR =>
-            msgs + (serial ->
-              Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin")))
+            msgs + (serial -> tooltip_text(List(msg)))
+          case (msgs, Text.Info(_,
+              XML.Elem(Markup(Isabelle_Markup.BAD, Isabelle_Markup.Message(msg)), _))) =>
+            msgs + (0L -> tooltip_text(YXML.parse_body(msg)))
         }).toList.flatMap(_.info)
     if (msgs.isEmpty) None else Some(cat_lines(msgs.iterator.map(_._2)))
   }
@@ -290,7 +297,6 @@
       Isabelle_Markup.ML_CHAR -> get_color("#D2691E"),
       Isabelle_Markup.ML_STRING -> get_color("#D2691E"),
       Isabelle_Markup.ML_COMMENT -> get_color("#8B0000"),
-      Isabelle_Markup.ML_MALFORMED -> get_color("#FF6A6A"),
       Isabelle_Markup.ANTIQ -> get_color("blue"))
 
   private val text_color_elements = Set.empty[String] ++ text_colors.keys
@@ -336,7 +342,7 @@
       Token.Kind.VERBATIM -> COMMENT3,
       Token.Kind.SPACE -> NULL,
       Token.Kind.COMMENT -> COMMENT1,
-      Token.Kind.UNPARSED -> INVALID
+      Token.Kind.ERROR -> INVALID
     ).withDefaultValue(NULL)
   }