--- 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)
}
--- 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 =
--- 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)
}