author Andreas Lochbihler Wed, 30 May 2012 10:04:05 +0200 changeset 48039 daab96c3e2a9 parent 48038 72a8506dd59b (current diff) parent 48027 69ba790960ba (diff) child 48040 4caf6cd063be child 48041 d60f6b41bf2d
merged
```--- a/src/HOL/Library/Multiset.thy	Wed May 30 09:54:53 2012 +0200
+++ b/src/HOL/Library/Multiset.thy	Wed May 30 10:04:05 2012 +0200
@@ -654,6 +654,221 @@
qed

+subsection {* The fold combinator *}
+
+text {*
+  The intended behaviour is
+  @{text "fold_mset f z {#x\<^isub>1, ..., x\<^isub>n#} = f x\<^isub>1 (\<dots> (f x\<^isub>n z)\<dots>)"}
+  if @{text f} is associative-commutative.
+*}
+
+text {*
+  The graph of @{text "fold_mset"}, @{text "z"}: the start element,
+  @{text "f"}: folding function, @{text "A"}: the multiset, @{text
+  "y"}: the result.
+*}
+inductive
+  fold_msetG :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b \<Rightarrow> bool"
+  for f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
+  and z :: 'b
+where
+  emptyI [intro]:  "fold_msetG f z {#} z"
+| insertI [intro]: "fold_msetG f z A y \<Longrightarrow> fold_msetG f z (A + {#x#}) (f x y)"
+
+inductive_cases empty_fold_msetGE [elim!]: "fold_msetG f z {#} x"
+inductive_cases insert_fold_msetGE: "fold_msetG f z (A + {#}) y"
+
+definition
+  fold_mset :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b" where
+  "fold_mset f z A = (THE x. fold_msetG f z A x)"
+
+lemma Diff1_fold_msetG:
+  "fold_msetG f z (A - {#x#}) y \<Longrightarrow> x \<in># A \<Longrightarrow> fold_msetG f z A (f x y)"
+apply (frule_tac x = x in fold_msetG.insertI)
+apply auto
+done
+
+lemma fold_msetG_nonempty: "\<exists>x. fold_msetG f z A x"
+apply (induct A)
+ apply blast
+apply clarsimp
+apply (drule_tac x = x in fold_msetG.insertI)
+apply auto
+done
+
+lemma fold_mset_empty[simp]: "fold_mset f z {#} = z"
+unfolding fold_mset_def by blast
+
+context comp_fun_commute
+begin
+
+lemma fold_msetG_insertE_aux:
+  "fold_msetG f z A y \<Longrightarrow> a \<in># A \<Longrightarrow> \<exists>y'. y = f a y' \<and> fold_msetG f z (A - {#a#}) y'"
+proof (induct set: fold_msetG)
+  case (insertI A y x) show ?case
+  proof (cases "x = a")
+    assume "x = a" with insertI show ?case by auto
+  next
+    assume "x \<noteq> a"
+    then obtain y' where y: "y = f a y'" and y': "fold_msetG f z (A - {#a#}) y'"
+      using insertI by auto
+    have "f x y = f a (f x y')"
+      unfolding y by (rule fun_left_comm)
+    moreover have "fold_msetG f z (A + {#x#} - {#a#}) (f x y')"
+      using y' and `x \<noteq> a`
+      by (simp add: diff_union_swap [symmetric] fold_msetG.insertI)
+    ultimately show ?case by fast
+  qed
+qed simp
+
+lemma fold_msetG_insertE:
+  assumes "fold_msetG f z (A + {#x#}) v"
+  obtains y where "v = f x y" and "fold_msetG f z A y"
+using assms by (auto dest: fold_msetG_insertE_aux [where a=x])
+
+lemma fold_msetG_determ:
+  "fold_msetG f z A x \<Longrightarrow> fold_msetG f z A y \<Longrightarrow> y = x"
+proof (induct arbitrary: y set: fold_msetG)
+  case (insertI A y x v)
+  from `fold_msetG f z (A + {#x#}) v`
+  obtain y' where "v = f x y'" and "fold_msetG f z A y'"
+    by (rule fold_msetG_insertE)
+  from `fold_msetG f z A y'` have "y' = y" by (rule insertI)
+  with `v = f x y'` show "v = f x y" by simp
+qed fast
+
+lemma fold_mset_equality: "fold_msetG f z A y \<Longrightarrow> fold_mset f z A = y"
+unfolding fold_mset_def by (blast intro: fold_msetG_determ)
+
+lemma fold_msetG_fold_mset: "fold_msetG f z A (fold_mset f z A)"
+proof -
+  from fold_msetG_nonempty fold_msetG_determ
+  have "\<exists>!x. fold_msetG f z A x" by (rule ex_ex1I)
+  then show ?thesis unfolding fold_mset_def by (rule theI')
+qed
+
+lemma fold_mset_insert:
+  "fold_mset f z (A + {#x#}) = f x (fold_mset f z A)"
+by (intro fold_mset_equality fold_msetG.insertI fold_msetG_fold_mset)
+
+lemma fold_mset_commute: "f x (fold_mset f z A) = fold_mset f (f x z) A"
+by (induct A) (auto simp: fold_mset_insert fun_left_comm [of x])
+
+lemma fold_mset_single [simp]: "fold_mset f z {#x#} = f x z"
+using fold_mset_insert [of z "{#}"] by simp
+
+lemma fold_mset_union [simp]:
+  "fold_mset f z (A+B) = fold_mset f (fold_mset f z A) B"
+proof (induct A)
+  case empty then show ?case by simp
+next
+  have "A + {#x#} + B = (A+B) + {#x#}" by (simp add: add_ac)
+  then have "fold_mset f z (A + {#x#} + B) = f x (fold_mset f z (A + B))"
+  also have "\<dots> = fold_mset f (fold_mset f z (A + {#x#})) B"
+  finally show ?case .
+qed
+
+lemma fold_mset_fusion:
+  assumes "comp_fun_commute g"
+  shows "(\<And>x y. h (g x y) = f x (h y)) \<Longrightarrow> h (fold_mset g w A) = fold_mset f (h w) A" (is "PROP ?P")
+proof -
+  interpret comp_fun_commute g by (fact assms)
+  show "PROP ?P" by (induct A) auto
+qed
+
+lemma fold_mset_rec:
+  assumes "a \<in># A"
+  shows "fold_mset f z A = f a (fold_mset f z (A - {#a#}))"
+proof -
+  from assms obtain A' where "A = A' + {#a#}"
+    by (blast dest: multi_member_split)
+  then show ?thesis by simp
+qed
+
+end
+
+text {*
+  A note on code generation: When defining some function containing a
+  subterm @{term"fold_mset F"}, code generation is not automatic. When
+  interpreting locale @{text left_commutative} with @{text F}, the
+  would be code thms for @{const fold_mset} become thms like
+  @{term"fold_mset F z {#} = z"} where @{text F} is not a pattern but
+  contains defined symbols, i.e.\ is not a code thm. Hence a separate
+  constant with its own code thms needs to be introduced for @{text
+  F}. See the image operator below.
+*}
+
+
+subsection {* Image *}
+
+definition image_mset :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
+  "image_mset f = fold_mset (op + o single o f) {#}"
+
+interpretation image_fun_commute: comp_fun_commute "op + o single o f" for f
+
+lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
+
+lemma image_mset_single [simp]: "image_mset f {#x#} = {#f x#}"
+
+lemma image_mset_insert:
+  "image_mset f (M + {#a#}) = image_mset f M + {#f a#}"
+
+lemma image_mset_union [simp]:
+  "image_mset f (M+N) = image_mset f M + image_mset f N"
+apply (induct N)
+ apply simp
+done
+
+lemma size_image_mset [simp]: "size (image_mset f M) = size M"
+by (induct M) simp_all
+
+lemma image_mset_is_empty_iff [simp]: "image_mset f M = {#} \<longleftrightarrow> M = {#}"
+by (cases M) auto
+
+syntax
+  "_comprehension1_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"
+      ("({#_/. _ :# _#})")
+translations
+  "{#e. x:#M#}" == "CONST image_mset (%x. e) M"
+
+syntax
+  "_comprehension2_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
+      ("({#_/ | _ :# _./ _#})")
+translations
+  "{#e | x:#M. P#}" => "{#e. x :# {# x:#M. P#}#}"
+
+text {*
+  This allows to write not just filters like @{term "{#x:#M. x<c#}"}
+  but also images like @{term "{#x+x. x:#M #}"} and @{term [source]
+  "{#x+x|x:#M. x<c#}"}, where the latter is currently displayed as
+  @{term "{#x+x|x:#M. x<c#}"}.
+*}
+
+enriched_type image_mset: image_mset
+proof -
+  fix f g show "image_mset f \<circ> image_mset g = image_mset (f \<circ> g)"
+  proof
+    fix A
+    show "(image_mset f \<circ> image_mset g) A = image_mset (f \<circ> g) A"
+      by (induct A) simp_all
+  qed
+  show "image_mset id = id"
+  proof
+    fix A
+    show "image_mset id A = id A"
+      by (induct A) simp_all
+  qed
+qed
+
+
subsection {* Alternative representations *}

subsubsection {* Lists *}
@@ -1456,221 +1671,6 @@
qed (auto simp add: le_multiset_def intro: union_less_mono2)

-subsection {* The fold combinator *}
-
-text {*
-  The intended behaviour is
-  @{text "fold_mset f z {#x\<^isub>1, ..., x\<^isub>n#} = f x\<^isub>1 (\<dots> (f x\<^isub>n z)\<dots>)"}
-  if @{text f} is associative-commutative.
-*}
-
-text {*
-  The graph of @{text "fold_mset"}, @{text "z"}: the start element,
-  @{text "f"}: folding function, @{text "A"}: the multiset, @{text
-  "y"}: the result.
-*}
-inductive
-  fold_msetG :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b \<Rightarrow> bool"
-  for f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
-  and z :: 'b
-where
-  emptyI [intro]:  "fold_msetG f z {#} z"
-| insertI [intro]: "fold_msetG f z A y \<Longrightarrow> fold_msetG f z (A + {#x#}) (f x y)"
-
-inductive_cases empty_fold_msetGE [elim!]: "fold_msetG f z {#} x"
-inductive_cases insert_fold_msetGE: "fold_msetG f z (A + {#}) y"
-
-definition
-  fold_mset :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b" where
-  "fold_mset f z A = (THE x. fold_msetG f z A x)"
-
-lemma Diff1_fold_msetG:
-  "fold_msetG f z (A - {#x#}) y \<Longrightarrow> x \<in># A \<Longrightarrow> fold_msetG f z A (f x y)"
-apply (frule_tac x = x in fold_msetG.insertI)
-apply auto
-done
-
-lemma fold_msetG_nonempty: "\<exists>x. fold_msetG f z A x"
-apply (induct A)
- apply blast
-apply clarsimp
-apply (drule_tac x = x in fold_msetG.insertI)
-apply auto
-done
-
-lemma fold_mset_empty[simp]: "fold_mset f z {#} = z"
-unfolding fold_mset_def by blast
-
-context comp_fun_commute
-begin
-
-lemma fold_msetG_insertE_aux:
-  "fold_msetG f z A y \<Longrightarrow> a \<in># A \<Longrightarrow> \<exists>y'. y = f a y' \<and> fold_msetG f z (A - {#a#}) y'"
-proof (induct set: fold_msetG)
-  case (insertI A y x) show ?case
-  proof (cases "x = a")
-    assume "x = a" with insertI show ?case by auto
-  next
-    assume "x \<noteq> a"
-    then obtain y' where y: "y = f a y'" and y': "fold_msetG f z (A - {#a#}) y'"
-      using insertI by auto
-    have "f x y = f a (f x y')"
-      unfolding y by (rule fun_left_comm)
-    moreover have "fold_msetG f z (A + {#x#} - {#a#}) (f x y')"
-      using y' and `x \<noteq> a`
-      by (simp add: diff_union_swap [symmetric] fold_msetG.insertI)
-    ultimately show ?case by fast
-  qed
-qed simp
-
-lemma fold_msetG_insertE:
-  assumes "fold_msetG f z (A + {#x#}) v"
-  obtains y where "v = f x y" and "fold_msetG f z A y"
-using assms by (auto dest: fold_msetG_insertE_aux [where a=x])
-
-lemma fold_msetG_determ:
-  "fold_msetG f z A x \<Longrightarrow> fold_msetG f z A y \<Longrightarrow> y = x"
-proof (induct arbitrary: y set: fold_msetG)
-  case (insertI A y x v)
-  from `fold_msetG f z (A + {#x#}) v`
-  obtain y' where "v = f x y'" and "fold_msetG f z A y'"
-    by (rule fold_msetG_insertE)
-  from `fold_msetG f z A y'` have "y' = y" by (rule insertI)
-  with `v = f x y'` show "v = f x y" by simp
-qed fast
-
-lemma fold_mset_equality: "fold_msetG f z A y \<Longrightarrow> fold_mset f z A = y"
-unfolding fold_mset_def by (blast intro: fold_msetG_determ)
-
-lemma fold_msetG_fold_mset: "fold_msetG f z A (fold_mset f z A)"
-proof -
-  from fold_msetG_nonempty fold_msetG_determ
-  have "\<exists>!x. fold_msetG f z A x" by (rule ex_ex1I)
-  then show ?thesis unfolding fold_mset_def by (rule theI')
-qed
-
-lemma fold_mset_insert:
-  "fold_mset f z (A + {#x#}) = f x (fold_mset f z A)"
-by (intro fold_mset_equality fold_msetG.insertI fold_msetG_fold_mset)
-
-lemma fold_mset_commute: "f x (fold_mset f z A) = fold_mset f (f x z) A"
-by (induct A) (auto simp: fold_mset_insert fun_left_comm [of x])
-
-lemma fold_mset_single [simp]: "fold_mset f z {#x#} = f x z"
-using fold_mset_insert [of z "{#}"] by simp
-
-lemma fold_mset_union [simp]:
-  "fold_mset f z (A+B) = fold_mset f (fold_mset f z A) B"
-proof (induct A)
-  case empty then show ?case by simp
-next
-  have "A + {#x#} + B = (A+B) + {#x#}" by (simp add: add_ac)
-  then have "fold_mset f z (A + {#x#} + B) = f x (fold_mset f z (A + B))"
-  also have "\<dots> = fold_mset f (fold_mset f z (A + {#x#})) B"
-  finally show ?case .
-qed
-
-lemma fold_mset_fusion:
-  assumes "comp_fun_commute g"
-  shows "(\<And>x y. h (g x y) = f x (h y)) \<Longrightarrow> h (fold_mset g w A) = fold_mset f (h w) A" (is "PROP ?P")
-proof -
-  interpret comp_fun_commute g by (fact assms)
-  show "PROP ?P" by (induct A) auto
-qed
-
-lemma fold_mset_rec:
-  assumes "a \<in># A"
-  shows "fold_mset f z A = f a (fold_mset f z (A - {#a#}))"
-proof -
-  from assms obtain A' where "A = A' + {#a#}"
-    by (blast dest: multi_member_split)
-  then show ?thesis by simp
-qed
-
-end
-
-text {*
-  A note on code generation: When defining some function containing a
-  subterm @{term"fold_mset F"}, code generation is not automatic. When
-  interpreting locale @{text left_commutative} with @{text F}, the
-  would be code thms for @{const fold_mset} become thms like
-  @{term"fold_mset F z {#} = z"} where @{text F} is not a pattern but
-  contains defined symbols, i.e.\ is not a code thm. Hence a separate
-  constant with its own code thms needs to be introduced for @{text
-  F}. See the image operator below.
-*}
-
-
-subsection {* Image *}
-
-definition image_mset :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
-  "image_mset f = fold_mset (op + o single o f) {#}"
-
-interpretation image_fun_commute: comp_fun_commute "op + o single o f" for f
-
-lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
-
-lemma image_mset_single [simp]: "image_mset f {#x#} = {#f x#}"
-
-lemma image_mset_insert:
-  "image_mset f (M + {#a#}) = image_mset f M + {#f a#}"
-
-lemma image_mset_union [simp]:
-  "image_mset f (M+N) = image_mset f M + image_mset f N"
-apply (induct N)
- apply simp
-done
-
-lemma size_image_mset [simp]: "size (image_mset f M) = size M"
-by (induct M) simp_all
-
-lemma image_mset_is_empty_iff [simp]: "image_mset f M = {#} \<longleftrightarrow> M = {#}"
-by (cases M) auto
-
-syntax
-  "_comprehension1_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"
-      ("({#_/. _ :# _#})")
-translations
-  "{#e. x:#M#}" == "CONST image_mset (%x. e) M"
-
-syntax
-  "_comprehension2_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
-      ("({#_/ | _ :# _./ _#})")
-translations
-  "{#e | x:#M. P#}" => "{#e. x :# {# x:#M. P#}#}"
-
-text {*
-  This allows to write not just filters like @{term "{#x:#M. x<c#}"}
-  but also images like @{term "{#x+x. x:#M #}"} and @{term [source]
-  "{#x+x|x:#M. x<c#}"}, where the latter is currently displayed as
-  @{term "{#x+x|x:#M. x<c#}"}.
-*}
-
-enriched_type image_mset: image_mset
-proof -
-  fix f g show "image_mset f \<circ> image_mset g = image_mset (f \<circ> g)"
-  proof
-    fix A
-    show "(image_mset f \<circ> image_mset g) A = image_mset (f \<circ> g) A"
-      by (induct A) simp_all
-  qed
-  show "image_mset id = id"
-  proof
-    fix A
-    show "image_mset id A = id A"
-      by (induct A) simp_all
-  qed
-qed
-
-
subsection {* Termination proofs with multiset orders *}

lemma multi_member_skip: "x \<in># XS \<Longrightarrow> x \<in># {# y #} + XS"```
```--- a/src/HOL/Tools/Lifting/lifting_def.ML	Wed May 30 09:54:53 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Wed May 30 10:04:05 2012 +0200
@@ -109,7 +109,7 @@
exception CODE_CERT_GEN of string

fun simplify_code_eq ctxt def_thm =
-  Local_Defs.unfold ctxt [@{thm o_def}, @{thm map_fun_def}, @{thm id_def}] def_thm
+  Local_Defs.unfold ctxt [@{thm o_apply}, @{thm map_fun_def}, @{thm id_apply}] def_thm

(*
quot_thm - quotient theorem (Quotient R Abs Rep T).```
```--- a/src/Pure/General/properties.scala	Wed May 30 09:54:53 2012 +0200
+++ b/src/Pure/General/properties.scala	Wed May 30 10:04:05 2012 +0200
@@ -52,7 +52,7 @@
props.find(_._1 == name).map(_._2)
}

-  class Int(name: java.lang.String)
+  class Int(val name: java.lang.String)
{
def apply(value: scala.Int): T = List((name, Value.Int(value)))
def unapply(props: T): Option[scala.Int] =
@@ -62,7 +62,7 @@
}
}

-  class Long(name: java.lang.String)
+  class Long(val name: java.lang.String)
{
def apply(value: scala.Long): T = List((name, Value.Long(value)))
def unapply(props: T): Option[scala.Long] =
@@ -72,7 +72,7 @@
}
}

-  class Double(name: java.lang.String)
+  class Double(val name: java.lang.String)
{
def apply(value: scala.Double): T = List((name, Value.Double(value)))
def unapply(props: T): Option[scala.Double] =```
```--- a/src/Pure/PIDE/isabelle_markup.scala	Wed May 30 09:54:53 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.scala	Wed May 30 10:04:05 2012 +0200
@@ -236,6 +236,8 @@
val STDERR = "stderr"
val EXIT = "exit"

+  val Return_Code = new Properties.Int("return_code")
+
val LEGACY = "legacy"

val NO_REPORT = "no_report"```
```--- a/src/Pure/System/gui_setup.scala	Wed May 30 09:54:53 2012 +0200
+++ b/src/Pure/System/gui_setup.scala	Wed May 30 10:04:05 2012 +0200
@@ -55,7 +55,7 @@
val isabelle_home_windows = Isabelle_System.getenv("ISABELLE_HOME_WINDOWS")
if (isabelle_home_windows != "")
text.append("Isabelle home (Windows): " + isabelle_home_windows + "\n")
-      text.append("Isabelle jdk home: " + Isabelle_System.getenv("ISABELLE_JDK_HOME") + "\n")
+      text.append("Isabelle JDK home: " + Isabelle_System.getenv("ISABELLE_JDK_HOME") + "\n")
}
catch { case ERROR(msg) => text.append(msg + "\n") }
```
```--- a/src/Pure/System/isabelle_process.scala	Wed May 30 09:54:53 2012 +0200
+++ b/src/Pure/System/isabelle_process.scala	Wed May 30 10:04:05 2012 +0200
@@ -77,7 +77,6 @@

class Isabelle_Process(
-    timeout: Time = Time.seconds(25),
receiver: Isabelle_Process.Message => Unit = Console.println(_),
args: List[String] = Nil)
{
@@ -104,9 +103,10 @@
}
}

-  private def output_message(kind: String, text: String)
+  private def exit_message(rc: Int)
{
-    output_message(kind, Nil, List(XML.Text(Symbol.decode(text))))
+    output_message(Isabelle_Markup.EXIT, Isabelle_Markup.Return_Code(rc),
+      List(XML.Text("Return code: " + rc.toString)))
}

@@ -154,25 +154,25 @@
{
val (startup_failed, startup_errors) =
{
-      val expired = System.currentTimeMillis() + timeout.ms
+      var finished: Option[Boolean] = None
val result = new StringBuilder(100)
-
-      var finished: Option[Boolean] = None
-      while (finished.isEmpty && System.currentTimeMillis() <= expired) {
+      while (finished.isEmpty && (process.stderr.ready || !process_result.is_finished)) {
-          if (c == 2) finished = Some(true)
-          else result += c.toChar
+          try {
+            if (c == 2) finished = Some(true)
+            else result += c.toChar
+          }
+          catch { case _: IOException => finished = Some(false) }
}
-        if (process_result.is_finished) finished = Some(false)
}
(finished.isEmpty || !finished.get, result.toString.trim)
}
if (startup_errors != "") system_output(startup_errors)

if (startup_failed) {
-      output_message(Isabelle_Markup.EXIT, "Return code: 127")
+      exit_message(127)
process.stdin.close
terminate_process()
@@ -189,10 +189,11 @@

val rc = process_result.join
system_output("process terminated")
+      close_input()
for ((thread, _) <- List(standard_input, stdout, stderr, command_input, message))
system_output("process_manager terminated")
-      output_message(Isabelle_Markup.EXIT, "Return code: " + rc.toString)
+      exit_message(rc)
}
system_channel.accepted()
}
@@ -204,7 +205,7 @@

def terminate()
{
-    close()
+    close_input()
system_output("Terminating Isabelle process")
terminate_process()
}
@@ -263,7 +264,7 @@
else done = true
}
if (result.length > 0) {
-            output_message(markup, result.toString)
+            output_message(markup, Nil, List(XML.Text(Symbol.decode(result.toString))))
result.length = 0
}
else {
@@ -399,5 +400,5 @@
input_bytes(name, args.map(Standard_System.string_bytes): _*)
}

-  def close(): Unit = { close(command_input); close(standard_input) }
+  def close_input(): Unit = { close(command_input); close(standard_input) }
}```
```--- a/src/Pure/System/session.scala	Wed May 30 09:54:53 2012 +0200
+++ b/src/Pure/System/session.scala	Wed May 30 10:04:05 2012 +0200
@@ -174,7 +174,7 @@

/* actor messages */

-  private case class Start(timeout: Time, args: List[String])
+  private case class Start(args: List[String])
private case object Cancel_Execution
private case class Edit(edits: List[Document.Edit_Text])
private case class Change(
@@ -369,10 +369,12 @@
case Isabelle_Markup.Keyword_Decl(name) if output.is_protocol =>
prover_syntax += name

+        case Isabelle_Markup.Return_Code(rc) if output.is_exit =>
+          if (rc == 0) phase = Session.Inactive
+          else phase = Session.Failed
+
case _ =>
-          if (output.is_exit && phase == Session.Startup) phase = Session.Failed
-          else if (output.is_exit) phase = Session.Inactive
-          else if (output.is_init || output.is_stdout) { }
+          if (output.is_init || output.is_stdout) { }
}
}
@@ -387,10 +389,10 @@
case TIMEOUT => delay_commands_changed.flush()

-        case Start(timeout, args) if prover.isEmpty =>
+        case Start(args) if prover.isEmpty =>
if (phase == Session.Inactive || phase == Session.Failed) {
phase = Session.Startup
-            prover = Some(new Isabelle_Process(timeout, receiver.invoke _, args) with Protocol)
+            prover = Some(new Isabelle_Process(receiver.invoke _, args) with Protocol)
}

case Stop =>
@@ -444,10 +446,7 @@

/* actions */

-  def start(timeout: Time, args: List[String])
-  { session_actor ! Start(timeout, args) }
-
-  def start(args: List[String]) { start (Time.seconds(25), args) }
+  def start(args: List[String]) { session_actor ! Start(args) }

def stop() { commands_changed_buffer !? Stop; change_parser !? Stop; session_actor !? Stop }
```
```--- a/src/Pure/System/standard_system.scala	Wed May 30 09:54:53 2012 +0200
+++ b/src/Pure/System/standard_system.scala	Wed May 30 10:04:05 2012 +0200
@@ -8,7 +8,6 @@
package isabelle

import java.lang.System
-import java.util.zip.{ZipEntry, ZipInputStream}
import java.util.regex.Pattern
import java.util.Locale
import java.net.URL
@@ -182,95 +181,6 @@
: (String, Int) = process_output(raw_execute(cwd, env, redirect, args: _*))

-  /* unpack zip archive -- platform file-system */
-
-  def unzip(url: URL, root: File)
-  {
-    import scala.collection.JavaConversions._
-
-    val buffer = new Array[Byte](4096)
-
-    val zip_stream = new ZipInputStream(new BufferedInputStream(url.openStream))
-    var entry: ZipEntry = null
-    try {
-      while ({ entry = zip_stream.getNextEntry; entry != null }) {
-        val file = new File(root, entry.getName.replace('/', File.separatorChar))
-        val dir = file.getParentFile
-        if (dir != null && !dir.isDirectory && !dir.mkdirs)
-          error("Failed to create directory: " + dir)
-
-        var len = 0
-        val out_stream = new BufferedOutputStream(new FileOutputStream(file))
-        try {
-          while ({ len = zip_stream.read(buffer); len != -1 })
-            out_stream.write(buffer, 0, len)
-        }
-        finally { out_stream.close }
-      }
-    }
-    finally { zip_stream.close }
-  }
-
-
-  /* unpack tar archive -- POSIX file-system */
-
-  def posix_untar(url: URL, root: File, gunzip: Boolean = false,
-    tar: String = "tar", gzip: String = "", progress: Int => Unit = _ => ()): String =
-  {
-    if (!root.isDirectory && !root.mkdirs)
-      error("Failed to create root directory: " + root)
-
-    val connection = url.openConnection
-
-    val length = connection.getContentLength.toLong
-    require(length >= 0L)
-
-    val stream = new BufferedInputStream(connection.getInputStream)
-    val progress_stream = new InputStream {
-      private val total = length max 1L
-      private var index = 0L
-      private var percentage = 0L
-      override def read(): Int =
-      {
-        if (c != -1) {
-          index += 100
-          val p = index / total
-          if (percentage != p) { percentage = p; progress(percentage.toInt) }
-        }
-        c
-      }
-      override def available(): Int = stream.available
-      override def close() { stream.close }
-    }
-
-    val cmdline =
-      List(tar, "-o", "-x", "-f-") :::
-        (if (!gunzip) Nil else if (gzip == "") List("-z") else List("-I", gzip))
-
-    val proc = raw_execute(root, null, false, cmdline:_*)
-    val stdout = Simple_Thread.future("tar_stdout") { slurp(proc.getInputStream) }
-    val stderr = Simple_Thread.future("tar_stderr") { slurp(proc.getErrorStream) }
-    val stdin = new BufferedOutputStream(proc.getOutputStream)
-
-    try {
-      var c = -1
-      val io_err =
-        try { while ({ c = progress_stream.read; c != -1 }) stdin.write(c); false }
-        catch { case e: IOException => true }
-      stdin.close
-
-      val rc = try { proc.waitFor } finally { Thread.interrupted }
-      if (io_err || rc != 0) error(stderr.join.trim) else stdout.join
-    }
-    finally {
-      progress_stream.close
-      stdin.close
-      proc.destroy
-    }
-  }
-
-
/* cygwin_root */

def cygwin_root(): String =```
```--- a/src/Tools/jEdit/lib/Tools/jedit	Wed May 30 09:54:53 2012 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Wed May 30 10:04:05 2012 +0200
@@ -22,8 +22,10 @@
"src/plugin.scala"
"src/protocol_dockable.scala"
"src/raw_output_dockable.scala"
"src/scala_console.scala"
"src/session_dockable.scala"
+  "src/syslog_dockable.scala"
"src/text_area_painter.scala"
"src/text_overview.scala"
"src/token_markup.scala"
@@ -260,7 +262,7 @@

if [ ! -e "\$JEDIT_SETTINGS/perspective.xml" ]; then
cat > "\$JEDIT_SETTINGS/DockableWindowManager/perspective-view0.xml" <<EOF
-<DOCKING LEFT="" TOP="" RIGHT="" BOTTOM="isabelle-session" LEFT_POS="0" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />
+<DOCKING LEFT="" TOP="" RIGHT="" BOTTOM="isabelle-readme" LEFT_POS="0" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />
EOF
cat > "\$JEDIT_SETTINGS/perspective.xml" <<EOF
<?xml version="1.0" encoding="UTF-8" ?>```
```--- a/src/Tools/jEdit/src/Isabelle.props	Wed May 30 09:54:53 2012 +0200
+++ b/src/Tools/jEdit/src/Isabelle.props	Wed May 30 10:04:05 2012 +0200
@@ -33,7 +33,6 @@
options.isabelle.tooltip-margin=60
options.isabelle.tooltip-dismiss-delay.title=Tooltip Dismiss Delay (global)
options.isabelle.tooltip-dismiss-delay=8.0
-options.isabelle.startup-timeout=25.0
options.isabelle.auto-start.title=Auto Start
options.isabelle.auto-start=true

@@ -51,17 +50,21 @@

isabelle.session-panel.label=Prover Session panel
isabelle.output-panel.label=Output panel
isabelle.raw-output-panel.label=Raw Output panel
isabelle.protocol-panel.label=Protocol panel
+isabelle.syslog-panel.label=Syslog panel

#dockables
isabelle-session.title=Prover Session
isabelle-output.title=Output
isabelle-raw-output.title=Raw Output
isabelle-protocol.title=Protocol
+isabelle-syslog.title=Syslog

#SideKick
sidekick.parser.isabelle.label=Isabelle```
```--- a/src/Tools/jEdit/src/actions.xml	Wed May 30 09:54:53 2012 +0200
+++ b/src/Tools/jEdit/src/actions.xml	Wed May 30 10:04:05 2012 +0200
@@ -7,6 +7,16 @@
</CODE>
</ACTION>
+	<ACTION NAME="isabelle.syslog-panel">
+		<CODE>
+		</CODE>
+	</ACTION>
+		<CODE>
+		</CODE>
+	</ACTION>
<ACTION NAME="isabelle.output-panel">
<CODE>
```--- a/src/Tools/jEdit/src/dockables.xml	Wed May 30 09:54:53 2012 +0200
+++ b/src/Tools/jEdit/src/dockables.xml	Wed May 30 10:04:05 2012 +0200
@@ -5,6 +5,12 @@
<DOCKABLE NAME="isabelle-session" MOVABLE="TRUE">
new isabelle.jedit.Session_Dockable(view, position);
</DOCKABLE>
+	<DOCKABLE NAME="isabelle-syslog" MOVABLE="TRUE">
+		new isabelle.jedit.Syslog_Dockable(view, position);
+	</DOCKABLE>
+	</DOCKABLE>
<DOCKABLE NAME="isabelle-output" MOVABLE="TRUE">
new isabelle.jedit.Output_Dockable(view, position);
</DOCKABLE>```
```--- a/src/Tools/jEdit/src/jEdit.props	Wed May 30 09:54:53 2012 +0200
+++ b/src/Tools/jEdit/src/jEdit.props	Wed May 30 10:04:05 2012 +0200
@@ -181,6 +181,7 @@
isabelle-output.height=174
isabelle-output.width=412
isabelle-session.dock-position=bottom
line-end.shortcut=END
line-home.shortcut=HOME
lookAndFeel=com.sun.java.swing.plaf.nimbus.NimbusLookAndFeel```
```--- a/src/Tools/jEdit/src/output_dockable.scala	Wed May 30 09:54:53 2012 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Wed May 30 10:04:05 2012 +0200
@@ -133,6 +133,7 @@
Isabelle.session.global_settings += main_actor
Isabelle.session.commands_changed += main_actor
Isabelle.session.caret_focus += main_actor
+    handle_update()
}

override def exit()
@@ -178,6 +179,4 @@

private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, tracing, auto_update, update)
-
-  handle_update()
}```
```--- a/src/Tools/jEdit/src/plugin.scala	Wed May 30 09:54:53 2012 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Wed May 30 10:04:05 2012 +0200
@@ -295,14 +295,13 @@

def start_session()
{
-    val timeout = Time_Property("startup-timeout", Time.seconds(25)) max Time.seconds(5)
val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _)
val logic = {
val logic = Property("logic")
if (logic != null && logic != "") logic
else Isabelle.default_logic()
}
-    session.start(timeout, modes ::: List(logic))
+    session.start(modes ::: List(logic))
}

@@ -388,9 +387,8 @@
phase match {
case Session.Failed =>
-                Library.error_dialog(jEdit.getActiveView,
-                  "Failed to start Isabelle process",
-                    Library.scrollable_text(Isabelle.session.current_syslog()))
+                Library.error_dialog(jEdit.getActiveView, "Prover process failure",
+                    "Isabelle Syslog", Library.scrollable_text(Isabelle.session.current_syslog()))
}

```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/readme_dockable.scala	Wed May 30 10:04:05 2012 +0200
@@ -0,0 +1,24 @@
+    Author:     Makarius
+
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import org.gjt.sp.jedit.View
+
+
+class README_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
+{
+  private val readme = new HTML_Panel("SansSerif", 14)
+
+}```
```--- a/src/Tools/jEdit/src/session_dockable.scala	Wed May 30 09:54:53 2012 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Wed May 30 10:04:05 2012 +0200
@@ -10,8 +10,7 @@
import isabelle._

import scala.actors.Actor._
-import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment,
-  ScrollPane, TabbedPane, Component, Swing}
+import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, Component}
import scala.swing.event.{ButtonClicked, MouseClicked, SelectionChanged}

import java.lang.System
@@ -24,15 +23,9 @@

class Session_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
{
-  /* main tabs */
+  /* status */

-  private val readme = new HTML_Panel("SansSerif", 14)
-
-  val status = new ListView(Nil: List[Document.Node.Name]) {
+  private val status = new ListView(Nil: List[Document.Node.Name]) {
listenTo(mouse.clicks)
reactions += {
case MouseClicked(_, point, _, clicks, _) if clicks == 2 =>
@@ -43,34 +36,20 @@
status.peer.setLayoutOrientation(JList.VERTICAL_WRAP)
status.selection.intervalMode = ListView.IntervalMode.Single

-  private val syslog = new TextArea(Isabelle.session.current_syslog())
-
-  private val tabs = new TabbedPane {
-    pages += new TabbedPane.Page("Theory Status", new ScrollPane(status))
-    pages += new TabbedPane.Page("System Log", new ScrollPane(syslog))
-
-    selection.index =
-    {
-      val index = Isabelle.Int_Property("session-panel.selection", 0)
-      if (index >= pages.length) 0 else index
-    }
-    listenTo(selection)
-    reactions += {
-      case SelectionChanged(_) =>
-        Isabelle.Int_Property("session-panel.selection") = selection.index
-    }
-  }
-
-  set_content(tabs)
+  set_content(status)

/* controls */

-  val session_phase = new Label(Isabelle.session.phase.toString)
+  private val session_phase = new Label(Isabelle.session.phase.toString)
session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
session_phase.tooltip = "Prover status"

+  private def handle_phase(phase: Session.Phase)
+  {
+    Swing_Thread.later { session_phase.text = " " + phase.toString + " " }
+  }
+
private val cancel = new Button("Cancel") {
reactions += { case ButtonClicked(_) => Isabelle.cancel_execution() }
}
@@ -173,15 +152,7 @@
private val main_actor = actor {
loop {
react {
-        case output: Isabelle_Process.Output =>
-          if (output.is_syslog)
-              val text = Isabelle.session.current_syslog()
-              if (text != syslog.text) syslog.text = text
-            }
-
-        case phase: Session.Phase =>
-          Swing_Thread.later { session_phase.text = " " + phase.toString + " " }
+        case phase: Session.Phase => handle_phase(phase)

case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))

@@ -190,17 +161,15 @@
}
}

-  override def init() {
-    Isabelle.session.syslog_messages += main_actor
-    Isabelle.session.phase_changed += main_actor
-    Isabelle.session.commands_changed += main_actor
+  override def init()
+  {
+    Isabelle.session.phase_changed += main_actor; handle_phase(Isabelle.session.phase)
+    Isabelle.session.commands_changed += main_actor; handle_update()
}

-  override def exit() {
-    Isabelle.session.syslog_messages -= main_actor
+  override def exit()
+  {
Isabelle.session.phase_changed -= main_actor
Isabelle.session.commands_changed -= main_actor
}
-
-  handle_update()
}```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/syslog_dockable.scala	Wed May 30 10:04:05 2012 +0200
@@ -0,0 +1,60 @@
+/*  Title:      Tools/jEdit/src/syslog_dockable.scala
+    Author:     Makarius
+
+Dockable window for syslog.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import scala.actors.Actor._
+import scala.swing.TextArea
+
+import java.lang.System
+
+import org.gjt.sp.jedit.View
+
+
+class Syslog_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
+{
+  /* GUI components */
+
+  private val syslog = new TextArea()
+
+  private def update_syslog()
+  {
+      val text = Isabelle.session.current_syslog()
+      if (text != syslog.text) syslog.text = text
+    }
+  }
+
+  set_content(syslog)
+
+
+  /* main actor */
+
+  private val main_actor = actor {
+    loop {
+      react {
+        case output: Isabelle_Process.Output =>
+          if (output.is_syslog) update_syslog()
+
+      }
+    }
+  }
+
+  override def init()
+  {
+    Isabelle.session.syslog_messages += main_actor
+    update_syslog()
+  }
+
+  override def exit()
+  {
+    Isabelle.session.syslog_messages -= main_actor
+  }
+}```