# HG changeset patch
# User paulson
# Date 1504129904 -3600
# Node ID ad0cefe1e9a9cdfec1dab066a351c74a69cc6018
# Parent  beb48215cda765ef8cd92e596c230c0f1563433b# Parent  8f12f7e0d99702bb7e65a773206aaeb9c528df13
merged

diff -r 8f12f7e0d997 -r ad0cefe1e9a9 src/HOL/Library/Tree_Multiset.thy
--- 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
 
diff -r 8f12f7e0d997 -r ad0cefe1e9a9 src/HOL/SMT.thy
--- 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>
diff -r 8f12f7e0d997 -r ad0cefe1e9a9 src/Pure/General/mercurial.scala
--- 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 =
   {
diff -r 8f12f7e0d997 -r ad0cefe1e9a9 src/Tools/jEdit/lib/Tools/jedit
--- 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=(
diff -r 8f12f7e0d997 -r ad0cefe1e9a9 src/Tools/jEdit/src-base/plugin.scala
--- 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)
   }
 }
diff -r 8f12f7e0d997 -r ad0cefe1e9a9 src/Tools/jEdit/src-base/syntax_style.scala
--- /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
+    }
+  }
+}