35 "isabelle-options", // etc/options |
35 "isabelle-options", // etc/options |
36 "isabelle-output", // pretty text area output |
36 "isabelle-output", // pretty text area output |
37 "isabelle-root", // session ROOT |
37 "isabelle-root", // session ROOT |
38 "sml") // Standard ML (not Isabelle/ML) |
38 "sml") // Standard ML (not Isabelle/ML) |
39 |
39 |
40 private lazy val ml_syntax: Outer_Syntax = |
40 private val ml_syntax: Outer_Syntax = |
41 Outer_Syntax.init.no_tokens. |
41 Outer_Syntax.empty.no_tokens. |
42 set_language_context(Completion.Language_Context.ML_outer) |
42 set_language_context(Completion.Language_Context.ML_outer) |
43 |
43 |
44 private lazy val sml_syntax: Outer_Syntax = |
44 private val sml_syntax: Outer_Syntax = |
45 Outer_Syntax.init.no_tokens. |
45 Outer_Syntax.empty.no_tokens. |
46 set_language_context(Completion.Language_Context.SML_outer) |
46 set_language_context(Completion.Language_Context.SML_outer) |
47 |
47 |
48 private lazy val news_syntax: Outer_Syntax = |
48 private val news_syntax: Outer_Syntax = |
49 Outer_Syntax.init.no_tokens |
49 Outer_Syntax.empty.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.session_base.overall_syntax) |
53 case "isabelle" => Some(PIDE.resources.session_base.overall_syntax) |
54 case "isabelle-options" => Some(Options.options_syntax) |
54 case "isabelle-options" => Some(Options.options_syntax) |