equal
deleted
inserted
replaced
31 "isabelle-output", // pretty text area output |
31 "isabelle-output", // pretty text area output |
32 "isabelle-root") // session ROOT |
32 "isabelle-root") // session ROOT |
33 |
33 |
34 private lazy val ml_syntax: Outer_Syntax = |
34 private lazy val ml_syntax: Outer_Syntax = |
35 Outer_Syntax.init().no_tokens. |
35 Outer_Syntax.init().no_tokens. |
36 set_completion_context(Completion.Context(Markup.Language.ML, false)) |
36 set_completion_context(Completion.Context.ML_outer) |
37 |
37 |
38 private lazy val news_syntax: Outer_Syntax = |
38 private lazy val news_syntax: Outer_Syntax = |
39 Outer_Syntax.init().no_tokens |
39 Outer_Syntax.init().no_tokens |
40 |
40 |
41 def mode_syntax(name: String): Option[Outer_Syntax] = |
41 def mode_syntax(name: String): Option[Outer_Syntax] = |