9 |
9 |
10 import isabelle._ |
10 import isabelle._ |
11 import org.gjt.sp.jedit.{ServiceManager, View} |
11 import org.gjt.sp.jedit.{ServiceManager, View} |
12 |
12 |
13 |
13 |
14 object Active |
14 object Active { |
15 { |
15 abstract class Handler { |
16 abstract class Handler |
|
17 { |
|
18 def handle( |
16 def handle( |
19 view: View, text: String, elem: XML.Elem, |
17 view: View, text: String, elem: XML.Elem, |
20 doc_view: Document_View, snapshot: Document.Snapshot): Boolean |
18 doc_view: Document_View, snapshot: Document.Snapshot): Boolean |
21 } |
19 } |
22 |
20 |
23 def handlers: List[Handler] = |
21 def handlers: List[Handler] = |
24 ServiceManager.getServiceNames(classOf[Handler]).toList |
22 ServiceManager.getServiceNames(classOf[Handler]).toList |
25 .map(ServiceManager.getService(classOf[Handler], _)) |
23 .map(ServiceManager.getService(classOf[Handler], _)) |
26 |
24 |
27 def action(view: View, text: String, elem: XML.Elem): Unit = |
25 def action(view: View, text: String, elem: XML.Elem): Unit = { |
28 { |
|
29 GUI_Thread.require {} |
26 GUI_Thread.require {} |
30 |
27 |
31 Document_View.get(view.getTextArea) match { |
28 Document_View.get(view.getTextArea) match { |
32 case Some(doc_view) => |
29 case Some(doc_view) => |
33 doc_view.rich_text_area.robust_body(()) { |
30 doc_view.rich_text_area.robust_body(()) { |
38 } |
35 } |
39 case None => |
36 case None => |
40 } |
37 } |
41 } |
38 } |
42 |
39 |
43 class Misc_Handler extends Active.Handler |
40 class Misc_Handler extends Active.Handler { |
44 { |
|
45 override def handle( |
41 override def handle( |
46 view: View, text: String, elem: XML.Elem, |
42 view: View, text: String, elem: XML.Elem, |
47 doc_view: Document_View, snapshot: Document.Snapshot): Boolean = |
43 doc_view: Document_View, snapshot: Document.Snapshot |
48 { |
44 ): Boolean = { |
49 val text_area = doc_view.text_area |
45 val text_area = doc_view.text_area |
50 val model = doc_view.model |
46 val model = doc_view.model |
51 val buffer = model.buffer |
47 val buffer = model.buffer |
52 |
48 |
53 elem match { |
49 elem match { |