equal
deleted
inserted
replaced
48 private lazy val news_syntax: Outer_Syntax = |
48 private lazy val news_syntax: Outer_Syntax = |
49 Outer_Syntax.init().no_tokens |
49 Outer_Syntax.init().no_tokens |
50 |
50 |
51 def mode_syntax(mode: String): Option[Outer_Syntax] = |
51 def mode_syntax(mode: String): Option[Outer_Syntax] = |
52 mode match { |
52 mode match { |
53 case "isabelle" => Some(PIDE.resources.base.syntax) |
53 case "isabelle" => Some(PIDE.resources.session_base.syntax) |
54 case "isabelle-options" => Some(Options.options_syntax) |
54 case "isabelle-options" => Some(Options.options_syntax) |
55 case "isabelle-root" => Some(Sessions.root_syntax) |
55 case "isabelle-root" => Some(Sessions.root_syntax) |
56 case "isabelle-ml" => Some(ml_syntax) |
56 case "isabelle-ml" => Some(ml_syntax) |
57 case "isabelle-news" => Some(news_syntax) |
57 case "isabelle-news" => Some(news_syntax) |
58 case "isabelle-output" => None |
58 case "isabelle-output" => None |