45 set_language_context(Completion.Language_Context.SML_outer) |
45 set_language_context(Completion.Language_Context.SML_outer) |
46 |
46 |
47 private lazy val news_syntax: Outer_Syntax = |
47 private lazy val news_syntax: Outer_Syntax = |
48 Outer_Syntax.init().no_tokens |
48 Outer_Syntax.init().no_tokens |
49 |
49 |
|
50 private lazy val bootstrap_syntax: Outer_Syntax = |
|
51 Thy_Header.bootstrap_syntax() |
|
52 |
50 def session_syntax(): Option[Outer_Syntax] = |
53 def session_syntax(): Option[Outer_Syntax] = |
51 PIDE.session.recent_syntax match { |
54 PIDE.session.recent_syntax match { |
52 case syntax: Outer_Syntax if syntax != Outer_Syntax.empty => Some(syntax) |
55 case syntax: Outer_Syntax if syntax != Outer_Syntax.empty => Some(syntax) |
53 case _ => None |
56 case _ => None |
54 } |
57 } |
55 |
58 |
56 def mode_syntax(name: String): Option[Outer_Syntax] = |
59 def mode_syntax(mode: String): Option[Outer_Syntax] = |
57 name match { |
60 mode match { |
58 case "isabelle" => session_syntax() |
61 case "isabelle" => Some(bootstrap_syntax) |
59 case "isabelle-options" => Some(Options.options_syntax) |
62 case "isabelle-options" => Some(Options.options_syntax) |
60 case "isabelle-root" => Some(Build.root_syntax) |
63 case "isabelle-root" => Some(Build.root_syntax) |
61 case "isabelle-ml" => Some(ml_syntax) |
64 case "isabelle-ml" => Some(ml_syntax) |
62 case "isabelle-news" => Some(news_syntax) |
65 case "isabelle-news" => Some(news_syntax) |
63 case "isabelle-output" => None |
66 case "isabelle-output" => None |
64 case "sml" => Some(sml_syntax) |
67 case "sml" => Some(sml_syntax) |
65 case _ => None |
68 case _ => None |
66 } |
69 } |
67 |
70 |
68 def buffer_syntax(buffer: JEditBuffer): Option[Outer_Syntax] = |
71 def buffer_syntax(buffer: JEditBuffer): Option[Outer_Syntax] = |
69 mode_syntax(JEdit_Lib.buffer_mode(buffer)) |
72 JEdit_Lib.buffer_mode(buffer) match { |
|
73 case "isabelle" => session_syntax() |
|
74 case mode => mode_syntax(mode) |
|
75 } |
70 |
76 |
71 |
77 |
72 /* token markers */ |
78 /* token markers */ |
73 |
79 |
74 private val markers: Map[String, TokenMarker] = |
80 private val mode_markers: Map[String, TokenMarker] = |
75 Map(modes.map(name => (name, new Token_Markup.Marker(name))): _*) + |
81 Map(modes.map(mode => (mode, new Token_Markup.Marker(mode, None))): _*) + |
76 ("bibtex" -> new Bibtex_JEdit.Token_Marker) |
82 ("bibtex" -> new Bibtex_JEdit.Token_Marker) |
77 |
83 |
78 def token_marker(name: String): Option[TokenMarker] = markers.get(name) |
84 def mode_token_marker(mode: String): Option[TokenMarker] = mode_markers.get(mode) |
|
85 |
|
86 def buffer_token_marker(buffer: Buffer): Option[TokenMarker] = |
|
87 { |
|
88 val mode = JEdit_Lib.buffer_mode(buffer) |
|
89 if (mode == "isabelle") Some(new Token_Markup.Marker(mode, Some(buffer))) |
|
90 else mode_token_marker(mode) |
|
91 } |
79 |
92 |
80 |
93 |
81 /* structure matchers */ |
94 /* structure matchers */ |
82 |
95 |
83 def structure_matchers(name: String): List[StructureMatcher] = |
96 def structure_matchers(name: String): List[StructureMatcher] = |