tuned;
authorwenzelm
Wed Sep 14 12:12:44 2016 +0200 (2016-09-14)
changeset 63865ccac33e291b1
parent 63863 d14e580c3b8f
child 63866 630eaf8fe9f3
tuned;
src/Pure/Isar/outer_syntax.scala
src/Pure/Tools/build.scala
src/Tools/jEdit/src/isabelle.scala
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Tue Sep 13 20:51:14 2016 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Wed Sep 14 12:12:44 2016 +0200
     1.3 @@ -94,8 +94,8 @@
     1.4    def ++ (other: Outer_Syntax): Outer_Syntax =
     1.5      if (this eq other) this
     1.6      else {
     1.7 -      val keywords1 = keywords ++ other.asInstanceOf[Outer_Syntax].keywords
     1.8 -      val completion1 = completion ++ other.asInstanceOf[Outer_Syntax].completion
     1.9 +      val keywords1 = keywords ++ other.keywords
    1.10 +      val completion1 = completion ++ other.completion
    1.11        if ((keywords eq keywords1) && (completion eq completion1)) this
    1.12        else new Outer_Syntax(keywords1, completion1, language_context, has_tokens)
    1.13      }
     2.1 --- a/src/Pure/Tools/build.scala	Tue Sep 13 20:51:14 2016 +0200
     2.2 +++ b/src/Pure/Tools/build.scala	Wed Sep 14 12:12:44 2016 +0200
     2.3 @@ -170,7 +170,7 @@
     2.4  
     2.5              val loaded_theories = thy_deps.loaded_theories
     2.6              val keywords = thy_deps.keywords
     2.7 -            val syntax = thy_deps.syntax.asInstanceOf[Outer_Syntax]
     2.8 +            val syntax = thy_deps.syntax
     2.9  
    2.10              val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
    2.11              val loaded_files =
     3.1 --- a/src/Tools/jEdit/src/isabelle.scala	Tue Sep 13 20:51:14 2016 +0200
     3.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Wed Sep 14 12:12:44 2016 +0200
     3.3 @@ -50,7 +50,7 @@
     3.4  
     3.5    def mode_syntax(mode: String): Option[Outer_Syntax] =
     3.6      mode match {
     3.7 -      case "isabelle" => Some(PIDE.resources.base_syntax.asInstanceOf[Outer_Syntax])
     3.8 +      case "isabelle" => Some(PIDE.resources.base_syntax)
     3.9        case "isabelle-options" => Some(Options.options_syntax)
    3.10        case "isabelle-root" => Some(Sessions.root_syntax)
    3.11        case "isabelle-ml" => Some(ml_syntax)
    3.12 @@ -63,7 +63,7 @@
    3.13    def buffer_syntax(buffer: JEditBuffer): Option[Outer_Syntax] =
    3.14      (JEdit_Lib.buffer_mode(buffer), PIDE.document_model(buffer)) match {
    3.15        case ("isabelle", Some(model)) =>
    3.16 -        Some(PIDE.session.recent_syntax(model.node_name).asInstanceOf[Outer_Syntax])
    3.17 +        Some(PIDE.session.recent_syntax(model.node_name))
    3.18        case (mode, _) => mode_syntax(mode)
    3.19      }
    3.20