--- a/src/HOL/Library/Tree_Multiset.thy Wed Aug 30 22:51:30 2017 +0100
+++ b/src/HOL/Library/Tree_Multiset.thy Wed Aug 30 22:51:44 2017 +0100
@@ -19,6 +19,9 @@
"subtrees_mset (Node l x r) = add_mset (Node l x r) (subtrees_mset l + subtrees_mset r)"
+lemma mset_tree_empty_iff[simp]: "mset_tree t = {#} \<longleftrightarrow> t = Leaf"
+by (cases t) auto
+
lemma set_mset_tree[simp]: "set_mset (mset_tree t) = set_tree t"
by(induction t) auto
@@ -40,7 +43,6 @@
lemma map_mirror: "mset_tree (mirror t) = mset_tree t"
by (induction t) (simp_all add: ac_simps)
-
lemma in_subtrees_mset_iff[simp]: "s \<in># subtrees_mset t \<longleftrightarrow> s \<in> subtrees t"
by(induction t) auto
--- a/src/HOL/SMT.thy Wed Aug 30 22:51:30 2017 +0100
+++ b/src/HOL/SMT.thy Wed Aug 30 22:51:44 2017 +0100
@@ -248,7 +248,7 @@
declare [[cvc3_options = ""]]
declare [[cvc4_options = "--full-saturate-quant --inst-when=full-last-call --inst-no-entail --term-db-mode=relevant --multi-trigger-linear"]]
-declare [[verit_options = ""]]
+declare [[verit_options = "--index-sorts --index-fresh-sorts"]]
declare [[z3_options = ""]]
text \<open>
--- a/src/Pure/General/mercurial.scala Wed Aug 30 22:51:30 2017 +0100
+++ b/src/Pure/General/mercurial.scala Wed Aug 30 22:51:44 2017 +0100
@@ -29,7 +29,15 @@
/* repository access */
def is_repository(root: Path, ssh: Option[SSH.Session] = None): Boolean =
- new Repository(root, ssh).command("root").ok
+ {
+ val root_hg = root + Path.explode(".hg")
+ val root_hg_present =
+ ssh match {
+ case None => root_hg.is_dir
+ case Some(ssh) => ssh.is_dir(root_hg)
+ }
+ root_hg_present && new Repository(root, ssh).command("root").ok
+ }
def repository(root: Path, ssh: Option[SSH.Session] = None): Repository =
{
--- a/src/Tools/jEdit/lib/Tools/jedit Wed Aug 30 22:51:30 2017 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Wed Aug 30 22:51:44 2017 +0100
@@ -22,6 +22,7 @@
declare -a SOURCES_BASE=(
"src-base/isabelle_encoding.scala"
"src-base/plugin.scala"
+ "src-base/syntax_style.scala"
)
declare -a RESOURCES_BASE=(
--- a/src/Tools/jEdit/src-base/plugin.scala Wed Aug 30 22:51:30 2017 +0100
+++ b/src/Tools/jEdit/src-base/plugin.scala Wed Aug 30 22:51:44 2017 +0100
@@ -10,6 +10,7 @@
import isabelle._
import org.gjt.sp.jedit.EBPlugin
+import org.gjt.sp.util.SyntaxUtilities
class Plugin extends EBPlugin
@@ -17,5 +18,7 @@
override def start()
{
Isabelle_System.init()
+
+ SyntaxUtilities.setStyleExtender(Syntax_Style.Dummy_Extender)
}
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src-base/syntax_style.scala Wed Aug 30 22:51:44 2017 +0100
@@ -0,0 +1,32 @@
+/* Title: Tools/jEdit/src-base/syntax_style.scala
+ Author: Makarius
+
+Extended syntax styles: dummy version.
+*/
+
+package isabelle.jedit_base
+
+
+import isabelle._
+
+import org.gjt.sp.util.SyntaxUtilities
+import org.gjt.sp.jedit.syntax.{Token => JEditToken, SyntaxStyle}
+
+
+object Syntax_Style
+{
+ private val plain_range: Int = JEditToken.ID_COUNT
+ private val full_range = 6 * plain_range + 1
+
+ object Dummy_Extender extends SyntaxUtilities.StyleExtender
+ {
+ override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
+ {
+ val new_styles = new Array[SyntaxStyle](full_range)
+ for (i <- 0 until full_range) {
+ new_styles(i) = styles(i % plain_range)
+ }
+ new_styles
+ }
+ }
+}