16 |
16 |
17 object Isabelle |
17 object Isabelle |
18 { |
18 { |
19 /* editor modes */ |
19 /* editor modes */ |
20 |
20 |
21 val modes = List("isabelle", "isabelle-options", "isabelle-root", "isabelle-news") |
21 val modes = |
|
22 List( |
|
23 "isabelle", // theory source |
|
24 "isabelle-news", // NEWS |
|
25 "isabelle-options", // etc/options |
|
26 "isabelle-output", // pretty text area output |
|
27 "isabelle-raw", // SideKick content tree |
|
28 "isabelle-root") // session ROOT |
22 |
29 |
23 private lazy val news_syntax = Outer_Syntax.init() |
30 private lazy val news_syntax = Outer_Syntax.init() |
24 |
31 |
25 def mode_syntax(name: String): Option[Outer_Syntax] = |
32 def mode_syntax(name: String): Option[Outer_Syntax] = |
26 name match { |
33 name match { |
27 case "isabelle" | "isabelle-raw" => PIDE.get_recent_syntax |
34 case "isabelle" | "isabelle-raw" => |
|
35 val syntax = PIDE.session.recent_syntax |
|
36 if (syntax == Outer_Syntax.empty) None else Some(syntax) |
28 case "isabelle-options" => Some(Options.options_syntax) |
37 case "isabelle-options" => Some(Options.options_syntax) |
29 case "isabelle-root" => Some(Build.root_syntax) |
38 case "isabelle-root" => Some(Build.root_syntax) |
30 case "isabelle-news" => Some(news_syntax) |
39 case "isabelle-news" => Some(news_syntax) |
|
40 case "isabelle-output" => None |
31 case _ => None |
41 case _ => None |
32 } |
42 } |
|
43 |
|
44 |
|
45 /* token markers */ |
|
46 |
|
47 private val marker_modes = |
|
48 List("isabelle", "isabelle-options", "isabelle-output", "isabelle-root") |
|
49 |
|
50 private val markers = |
|
51 Map(marker_modes.map(name => (name, new Token_Markup.Marker(name))): _*) |
|
52 |
|
53 def token_marker(name: String): Option[Token_Markup.Marker] = markers.get(name) |
33 |
54 |
34 |
55 |
35 /* dockable windows */ |
56 /* dockable windows */ |
36 |
57 |
37 private def wm(view: View): DockableWindowManager = view.getDockableWindowManager |
58 private def wm(view: View): DockableWindowManager = view.getDockableWindowManager |