# HG changeset patch # User Andreas Lochbihler # Date 1338365045 -7200 # Node ID daab96c3e2a9d72a692efadaa86022c077c02772 # Parent 72a8506dd59bfcda85b08be427ba0f7f610c69f9# Parent 69ba790960ba37734793704200cd5a777ebff703 merged diff -r 72a8506dd59b -r daab96c3e2a9 src/HOL/Library/Multiset.thy --- 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 (\ (f x\<^isub>n z)\)"} + 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 \ 'b \ 'b) \ 'b \ 'a multiset \ 'b \ bool" + for f :: "'a \ 'b \ 'b" + and z :: 'b +where + emptyI [intro]: "fold_msetG f z {#} z" +| insertI [intro]: "fold_msetG f z A y \ 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 \ 'b \ 'b) \ 'b \ 'a multiset \ '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 \ x \# A \ fold_msetG f z A (f x y)" +apply (frule_tac x = x in fold_msetG.insertI) +apply auto +done + +lemma fold_msetG_nonempty: "\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 \ a \# A \ \y'. y = f a y' \ 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 \ 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 \ 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 \ fold_msetG f z A y \ 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 \ 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 "\!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 "\ = 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 "(\x y. h (g x y) = f x (h y)) \ 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 \# 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 \ 'b) \ 'a multiset \ '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 = {#} \ M = {#}" +by (cases M) auto + +syntax + "_comprehension1_mset" :: "'a \ 'b \ 'b multiset \ 'a multiset" + ("({#_/. _ :# _#})") +translations + "{#e. x:#M#}" == "CONST image_mset (%x. e) M" + +syntax + "_comprehension2_mset" :: "'a \ 'b \ 'b multiset \ bool \ '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 image_mset g = image_mset (f \ g)" + proof + fix A + show "(image_mset f \ image_mset g) A = image_mset (f \ 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 (\ (f x\<^isub>n z)\)"} - 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 \ 'b \ 'b) \ 'b \ 'a multiset \ 'b \ bool" - for f :: "'a \ 'b \ 'b" - and z :: 'b -where - emptyI [intro]: "fold_msetG f z {#} z" -| insertI [intro]: "fold_msetG f z A y \ 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 \ 'b \ 'b) \ 'b \ 'a multiset \ '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 \ x \# A \ fold_msetG f z A (f x y)" -apply (frule_tac x = x in fold_msetG.insertI) -apply auto -done - -lemma fold_msetG_nonempty: "\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 \ a \# A \ \y'. y = f a y' \ 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 \ 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 \ 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 \ fold_msetG f z A y \ 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 \ 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 "\!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 "\ = 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 "(\x y. h (g x y) = f x (h y)) \ 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 \# 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 \ 'b) \ 'a multiset \ '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 = {#} \ M = {#}" -by (cases M) auto - -syntax - "_comprehension1_mset" :: "'a \ 'b \ 'b multiset \ 'a multiset" - ("({#_/. _ :# _#})") -translations - "{#e. x:#M#}" == "CONST image_mset (%x. e) M" - -syntax - "_comprehension2_mset" :: "'a \ 'b \ 'b multiset \ bool \ '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 image_mset g = image_mset (f \ g)" - proof - fix A - show "(image_mset f \ image_mset g) A = image_mset (f \ 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 \# XS \ x \# {# y #} + XS" diff -r 72a8506dd59b -r daab96c3e2a9 src/HOL/Tools/Lifting/lifting_def.ML --- 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). diff -r 72a8506dd59b -r daab96c3e2a9 src/Pure/General/properties.scala --- 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] = diff -r 72a8506dd59b -r daab96c3e2a9 src/Pure/PIDE/isabelle_markup.scala --- 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" diff -r 72a8506dd59b -r daab96c3e2a9 src/Pure/System/gui_setup.scala --- 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") } diff -r 72a8506dd59b -r daab96c3e2a9 src/Pure/System/isabelle_process.scala --- 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) } } diff -r 72a8506dd59b -r daab96c3e2a9 src/Pure/System/session.scala --- 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 } diff -r 72a8506dd59b -r daab96c3e2a9 src/Pure/System/standard_system.scala --- 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 = diff -r 72a8506dd59b -r daab96c3e2a9 src/Tools/jEdit/lib/Tools/jedit --- 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 cat > "$JEDIT_SETTINGS/perspective.xml" < diff -r 72a8506dd59b -r daab96c3e2a9 src/Tools/jEdit/src/Isabelle.props --- 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 diff -r 72a8506dd59b -r daab96c3e2a9 src/Tools/jEdit/src/actions.xml --- 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"); + + + wm.addDockableWindow("isabelle-syslog"); + + + + + wm.addDockableWindow("isabelle-readme"); + + wm.addDockableWindow("isabelle-output"); diff -r 72a8506dd59b -r daab96c3e2a9 src/Tools/jEdit/src/dockables.xml --- 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 @@ new isabelle.jedit.Session_Dockable(view, position); + + new isabelle.jedit.Syslog_Dockable(view, position); + + + new isabelle.jedit.README_Dockable(view, position); + new isabelle.jedit.Output_Dockable(view, position); diff -r 72a8506dd59b -r daab96c3e2a9 src/Tools/jEdit/src/jEdit.props --- 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 diff -r 72a8506dd59b -r daab96c3e2a9 src/Tools/jEdit/src/output_dockable.scala --- 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() } diff -r 72a8506dd59b -r daab96c3e2a9 src/Tools/jEdit/src/plugin.scala --- 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 => diff -r 72a8506dd59b -r daab96c3e2a9 src/Tools/jEdit/src/readme_dockable.scala --- /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) +} diff -r 72a8506dd59b -r daab96c3e2a9 src/Tools/jEdit/src/session_dockable.scala --- 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() } diff -r 72a8506dd59b -r daab96c3e2a9 src/Tools/jEdit/src/syslog_dockable.scala --- /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 + } +}