--- 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
+ case (add A x)
+ 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))"
+ by (simp add: fold_mset_insert)
+ also have "\<dots> = fold_mset f (fold_mset f z (A + {#x#})) B"
+ by (simp add: fold_mset_commute[of x,symmetric] add fold_mset_insert)
+ 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
+proof qed (simp add: add_ac fun_eq_iff)
+
+lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
+by (simp add: image_mset_def)
+
+lemma image_mset_single [simp]: "image_mset f {#x#} = {#f x#}"
+by (simp add: image_mset_def)
+
+lemma image_mset_insert:
+ "image_mset f (M + {#a#}) = image_mset f M + {#f a#}"
+by (simp add: image_mset_def add_ac)
+
+lemma image_mset_union [simp]:
+ "image_mset f (M+N) = image_mset f M + image_mset f N"
+apply (induct N)
+ apply simp
+apply (simp add: add_assoc [symmetric] image_mset_insert)
+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
- case (add A x)
- 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))"
- by (simp add: fold_mset_insert)
- also have "\<dots> = fold_mset f (fold_mset f z (A + {#x#})) B"
- by (simp add: fold_mset_commute[of x,symmetric] add fold_mset_insert)
- 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
-proof qed (simp add: add_ac fun_eq_iff)
-
-lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
-by (simp add: image_mset_def)
-
-lemma image_mset_single [simp]: "image_mset f {#x#} = {#f x#}"
-by (simp add: image_mset_def)
-
-lemma image_mset_insert:
- "image_mset f (M + {#a#}) = image_mset f M + {#f a#}"
-by (simp add: image_mset_def add_ac)
-
-lemma image_mset_union [simp]:
- "image_mset f (M+N) = image_mset f M + image_mset f N"
-apply (induct N)
- apply simp
-apply (simp add: add_assoc [symmetric] image_mset_insert)
-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)) {
while (finished.isEmpty && process.stderr.ready) {
- val c = process.stderr.read
- if (c == 2) finished = Some(true)
- else result += c.toChar
+ try {
+ val c = process.stderr.read
+ if (c == 2) finished = Some(true)
+ else result += c.toChar
+ }
+ catch { case _: IOException => finished = Some(false) }
}
- if (process_result.is_finished) finished = Some(false)
- else Thread.sleep(10)
+ Thread.sleep(10)
}
(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
Thread.sleep(300)
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))
thread.join
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) { }
else bad_output(output)
}
}
@@ -387,10 +389,10 @@
receiveWithin(delay_commands_changed.flush_timeout) {
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 =
- {
- val c = stream.read
- 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/readme_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 @@
#menu actions
plugin.isabelle.jedit.Plugin.menu.label=Isabelle
-plugin.isabelle.jedit.Plugin.menu=isabelle.session-panel isabelle.output-panel isabelle.raw-output-panel isabelle.protocol-panel
+plugin.isabelle.jedit.Plugin.menu=isabelle.session-panel isabelle.output-panel isabelle.raw-output-panel isabelle.protocol-panel isabelle.readme-panel isabelle.syslog-panel
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.readme-panel.label=README 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-readme.title=README
+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 @@
wm.addDockableWindow("isabelle-session");
</CODE>
</ACTION>
+ <ACTION NAME="isabelle.syslog-panel">
+ <CODE>
+ wm.addDockableWindow("isabelle-syslog");
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.readme-panel">
+ <CODE>
+ wm.addDockableWindow("isabelle-readme");
+ </CODE>
+ </ACTION>
<ACTION NAME="isabelle.output-panel">
<CODE>
wm.addDockableWindow("isabelle-output");
--- 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 NAME="isabelle-readme" MOVABLE="TRUE">
+ new isabelle.jedit.README_Dockable(view, position);
+ </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
+isabelle-readme.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)
add(controls.peer, BorderLayout.NORTH)
-
- 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 =>
Swing_Thread.later {
- 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()))
}
case Session.Ready =>
--- /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 @@
+/* Title: Tools/jEdit/src/readme_dockable.scala
+ Author: Makarius
+
+Dockable window for README.
+*/
+
+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)
+ private val readme_path = Path.explode("$JEDIT_HOME/README.html")
+ readme.render_document(
+ Isabelle_System.platform_file_url(readme_path),
+ Isabelle_System.try_read(List(readme_path)))
+
+ set_content(readme)
+}
--- 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)
- private val readme_path = Path.explode("$JEDIT_HOME/README.html")
- readme.render_document(
- Isabelle_System.platform_file_url(readme_path),
- Isabelle_System.try_read(List(readme_path)))
-
- 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("README", Component.wrap(readme))
- 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)
- Swing_Thread.later {
- 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()
+ {
+ Swing_Thread.later {
+ 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()
+
+ case bad => System.err.println("Syslog_Dockable: ignoring bad message " + bad)
+ }
+ }
+ }
+
+ override def init()
+ {
+ Isabelle.session.syslog_messages += main_actor
+ update_syslog()
+ }
+
+ override def exit()
+ {
+ Isabelle.session.syslog_messages -= main_actor
+ }
+}