equal
deleted
inserted
replaced
49 |
49 |
50 def mode_syntax(mode: String): Option[Outer_Syntax] = |
50 def mode_syntax(mode: String): Option[Outer_Syntax] = |
51 mode match { |
51 mode match { |
52 case "isabelle" => Some(PIDE.resources.base_syntax.asInstanceOf[Outer_Syntax]) |
52 case "isabelle" => Some(PIDE.resources.base_syntax.asInstanceOf[Outer_Syntax]) |
53 case "isabelle-options" => Some(Options.options_syntax) |
53 case "isabelle-options" => Some(Options.options_syntax) |
54 case "isabelle-root" => Some(Build.root_syntax) |
54 case "isabelle-root" => Some(Sessions.root_syntax) |
55 case "isabelle-ml" => Some(ml_syntax) |
55 case "isabelle-ml" => Some(ml_syntax) |
56 case "isabelle-news" => Some(news_syntax) |
56 case "isabelle-news" => Some(news_syntax) |
57 case "isabelle-output" => None |
57 case "isabelle-output" => None |
58 case "sml" => Some(sml_syntax) |
58 case "sml" => Some(sml_syntax) |
59 case _ => None |
59 case _ => None |