60 val text = server.resources.output_pretty_message(Pretty.separate(body)) |
60 val text = server.resources.output_pretty_message(Pretty.separate(body)) |
61 val content = |
61 val content = |
62 HTML.output_document( |
62 HTML.output_document( |
63 List(HTML.style(HTML.fonts_css()), |
63 List(HTML.style(HTML.fonts_css()), |
64 HTML.style_file(Url.print_file(HTML.isabelle_css.file))), |
64 HTML.style_file(Url.print_file(HTML.isabelle_css.file))), |
65 List( |
65 List(controls, HTML.source(text)), |
66 HTML.chapter("Proof state"), |
|
67 HTML.source(text)), |
|
68 css = "") |
66 css = "") |
69 output(content) |
67 output(content) |
70 }) |
68 }) |
71 |
69 |
72 def locate() { print_state.locate_query() } |
70 def locate() { print_state.locate_query() } |
91 def set_auto_update(b: Boolean) { auto_update_enabled.change(_ => b); if (b) update() } |
89 def set_auto_update(b: Boolean) { auto_update_enabled.change(_ => b); if (b) update() } |
92 |
90 |
93 def auto_update() { if (auto_update_enabled.value) update() } |
91 def auto_update() { if (auto_update_enabled.value) update() } |
94 |
92 |
95 |
93 |
|
94 /* controls */ |
|
95 |
|
96 private def id_parameter: XML.Elem = |
|
97 HTML.GUI.parameter(id.toString, name = "id") |
|
98 |
|
99 private def auto_update_button: XML.Elem = |
|
100 HTML.GUI.checkbox(HTML.text("Auto update"), |
|
101 name = "auto_update", |
|
102 tooltip = "Indicate automatic update following cursor movement", |
|
103 submit = true, |
|
104 selected = auto_update_enabled.value) |
|
105 |
|
106 private def update_button: XML.Elem = |
|
107 HTML.GUI.button(List(HTML.bold(HTML.text("Update"))), |
|
108 name = "update", |
|
109 tooltip = "Update display according to the command at cursor position", |
|
110 submit = true) |
|
111 |
|
112 private def locate_button: XML.Elem = |
|
113 HTML.GUI.button(HTML.text("Locate"), |
|
114 name = "locate", |
|
115 tooltip = "Locate printed command within source text", |
|
116 submit = true) |
|
117 |
|
118 private val controls: XML.Elem = |
|
119 HTML.Wrap_Panel( |
|
120 contents = List(id_parameter, auto_update_button, update_button, locate_button), |
|
121 alignment = HTML.Wrap_Panel.Alignment.right) |
|
122 |
|
123 |
96 /* main */ |
124 /* main */ |
97 |
125 |
98 private val main = |
126 private val main = |
99 Session.Consumer[Any](getClass.getName) { |
127 Session.Consumer[Any](getClass.getName) { |
100 case changed: Session.Commands_Changed => |
128 case changed: Session.Commands_Changed => |