# HG changeset patch
# User wenzelm
# Date 1473847964 -7200
# Node ID ccac33e291b1243fba3bee865f4beb004915c65f
# Parent  d14e580c3b8fb69a2a7ee3cf4653fee9030ef040
tuned;

diff -r d14e580c3b8f -r ccac33e291b1 src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Tue Sep 13 20:51:14 2016 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Wed Sep 14 12:12:44 2016 +0200
@@ -94,8 +94,8 @@
   def ++ (other: Outer_Syntax): Outer_Syntax =
     if (this eq other) this
     else {
-      val keywords1 = keywords ++ other.asInstanceOf[Outer_Syntax].keywords
-      val completion1 = completion ++ other.asInstanceOf[Outer_Syntax].completion
+      val keywords1 = keywords ++ other.keywords
+      val completion1 = completion ++ other.completion
       if ((keywords eq keywords1) && (completion eq completion1)) this
       else new Outer_Syntax(keywords1, completion1, language_context, has_tokens)
     }
diff -r d14e580c3b8f -r ccac33e291b1 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Sep 13 20:51:14 2016 +0200
+++ b/src/Pure/Tools/build.scala	Wed Sep 14 12:12:44 2016 +0200
@@ -170,7 +170,7 @@
 
             val loaded_theories = thy_deps.loaded_theories
             val keywords = thy_deps.keywords
-            val syntax = thy_deps.syntax.asInstanceOf[Outer_Syntax]
+            val syntax = thy_deps.syntax
 
             val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
             val loaded_files =
diff -r d14e580c3b8f -r ccac33e291b1 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Tue Sep 13 20:51:14 2016 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Wed Sep 14 12:12:44 2016 +0200
@@ -50,7 +50,7 @@
 
   def mode_syntax(mode: String): Option[Outer_Syntax] =
     mode match {
-      case "isabelle" => Some(PIDE.resources.base_syntax.asInstanceOf[Outer_Syntax])
+      case "isabelle" => Some(PIDE.resources.base_syntax)
       case "isabelle-options" => Some(Options.options_syntax)
       case "isabelle-root" => Some(Sessions.root_syntax)
       case "isabelle-ml" => Some(ml_syntax)
@@ -63,7 +63,7 @@
   def buffer_syntax(buffer: JEditBuffer): Option[Outer_Syntax] =
     (JEdit_Lib.buffer_mode(buffer), PIDE.document_model(buffer)) match {
       case ("isabelle", Some(model)) =>
-        Some(PIDE.session.recent_syntax(model.node_name).asInstanceOf[Outer_Syntax])
+        Some(PIDE.session.recent_syntax(model.node_name))
       case (mode, _) => mode_syntax(mode)
     }