--- a/src/Pure/GUI/wrap_panel.scala Tue Jun 27 15:10:13 2017 +0100
+++ b/src/Pure/GUI/wrap_panel.scala Tue Jun 27 23:21:30 2017 +0200
@@ -100,18 +100,19 @@
}
}
}
+
+ def apply(contents: List[Component] = Nil,
+ alignment: Alignment.Value = Alignment.Right): Wrap_Panel =
+ new Wrap_Panel(contents, alignment)
}
-
-class Wrap_Panel(alignment: Wrap_Panel.Alignment.Value)(contents0: Component*)
+class Wrap_Panel(contents0: List[Component] = Nil,
+ alignment: Wrap_Panel.Alignment.Value = Wrap_Panel.Alignment.Right)
extends Panel with SequentialContainer.Wrapper
{
override lazy val peer: JPanel =
new JPanel(new Wrap_Panel.Layout(alignment.id)) with SuperMixin
- def this(contents0: Component*) = this(Wrap_Panel.Alignment.Center)(contents0: _*)
- def this() = this(Wrap_Panel.Alignment.Center)()
-
contents ++= contents0
private def layoutManager = peer.getLayout.asInstanceOf[Wrap_Panel.Layout]
--- a/src/Pure/General/http.scala Tue Jun 27 15:10:13 2017 +0100
+++ b/src/Pure/General/http.scala Tue Jun 27 23:21:30 2017 +0200
@@ -7,7 +7,7 @@
package isabelle
-import java.net.{InetAddress, InetSocketAddress, URI}
+import java.net.{InetAddress, InetSocketAddress, URI, URLDecoder}
import com.sun.net.httpserver.{HttpExchange, HttpHandler, HttpServer}
import scala.collection.immutable.SortedMap
@@ -66,12 +66,28 @@
def handler(root: String, body: Exchange => Unit): Handler =
new Handler(root, new HttpHandler { def handle(x: HttpExchange) { body(new Exchange(x)) } })
- def get(root: String, body: URI => Option[Response]): Handler =
+
+ /* particular methods */
+
+ sealed case class Arg(method: String, uri: URI, request: Bytes)
+ {
+ def decode_properties: Properties.T =
+ Library.space_explode('&', request.text).map(s =>
+ Library.space_explode('=', s) match {
+ case List(a, b) =>
+ URLDecoder.decode(a, UTF8.charset_name) ->
+ URLDecoder.decode(b, UTF8.charset_name)
+ case _ => error("Malformed key-value pair in HTTP/POST: " + quote(s))
+ })
+ }
+
+ def method(name: String, root: String, body: Arg => Option[Response]): Handler =
handler(root, http =>
{
- http.read_request()
- if (http.request_method == "GET")
- Exn.capture(body(http.request_uri)) match {
+ val request = http.read_request()
+ if (http.request_method == name) {
+ val arg = Arg(name, http.request_uri, request)
+ Exn.capture(body(arg)) match {
case Exn.Res(Some(response)) =>
http.write_response(200, response)
case Exn.Res(None) =>
@@ -80,9 +96,13 @@
http.write_response(500, Response.text(Output.error_message_text(msg)))
case Exn.Exn(exn) => throw exn
}
+ }
else http.write_response(400, Response.empty)
})
+ def get(root: String, body: Arg => Option[Response]): Handler = method("GET", root, body)
+ def post(root: String, body: Arg => Option[Response]): Handler = method("POST", root, body)
+
/* server */
--- a/src/Pure/Thy/html.scala Tue Jun 27 15:10:13 2017 +0100
+++ b/src/Pure/Thy/html.scala Tue Jun 27 23:21:30 2017 +0200
@@ -279,6 +279,25 @@
}
+ /* GUI layout */
+
+ object Wrap_Panel
+ {
+ object Alignment extends Enumeration
+ {
+ val left, right, center = Value
+ }
+
+ def apply(contents: List[XML.Elem], name: String = "", action: String = "",
+ alignment: Alignment.Value = Alignment.right): XML.Elem =
+ {
+ val body = Library.separate(XML.Text(" "), contents)
+ GUI.form(List(div(body) + ("style" -> ("text-align: " + alignment))),
+ name = name, action = action)
+ }
+ }
+
+
/* document */
val header: String =
--- a/src/Tools/Graphview/graph_panel.scala Tue Jun 27 15:10:13 2017 +0100
+++ b/src/Tools/Graphview/graph_panel.scala Tue Jun 27 23:21:30 2017 +0200
@@ -345,8 +345,9 @@
private val filters = new Button { action = Action("Filters") { mutator_dialog.open } }
private val controls =
- new Wrap_Panel(Wrap_Panel.Alignment.Right)(show_content, show_arrow_heads, show_dummies,
- save_image, zoom, fit_window, update_layout, editor_style) // FIXME colorations, filters
+ Wrap_Panel(
+ List(show_content, show_arrow_heads, show_dummies,
+ save_image, zoom, fit_window, update_layout, editor_style)) // FIXME colorations, filters
--- a/src/Tools/Graphview/tree_panel.scala Tue Jun 27 15:10:13 2017 +0100
+++ b/src/Tools/Graphview/tree_panel.scala Tue Jun 27 23:21:30 2017 +0200
@@ -143,7 +143,7 @@
}
private val controls =
- new Wrap_Panel(Wrap_Panel.Alignment.Right)(selection_label, selection_field, selection_apply)
+ Wrap_Panel(List(selection_label, selection_field, selection_apply))
/* main layout */
--- a/src/Tools/VSCode/extension/package.json Tue Jun 27 15:10:13 2017 +0100
+++ b/src/Tools/VSCode/extension/package.json Tue Jun 27 23:21:30 2017 +0200
@@ -492,11 +492,11 @@
"postinstall": "node ./node_modules/vscode/bin/install"
},
"devDependencies": {
- "typescript": "^2.3.2",
- "vscode": "^1.1.0",
+ "@types/mocha": "^2.2.41",
+ "@types/node": "^7.0.32",
"mocha": "^3.4.1",
- "@types/node": "^7.0.21",
- "@types/mocha": "^2.2.41"
+ "typescript": "^2.4.1",
+ "vscode": "^1.1.1"
},
"dependencies": {
"vscode-languageclient": "~3.2.2"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/src/preview_panel.ts Tue Jun 27 23:21:30 2017 +0200
@@ -0,0 +1,96 @@
+'use strict';
+
+import * as timers from 'timers'
+import { ViewColumn, TextDocument, TextEditor, TextDocumentContentProvider,
+ ExtensionContext, Event, EventEmitter, Uri, Position, workspace,
+ window, commands } from 'vscode'
+import { LanguageClient } from 'vscode-languageclient';
+import * as library from './library'
+import * as protocol from './protocol'
+import { Content_Provider } from './content_provider'
+
+
+/* HTML content */
+
+const content_provider = new Content_Provider("isabelle-preview")
+
+function encode_preview(document_uri: Uri | undefined): Uri | undefined
+{
+ if (document_uri && library.is_file(document_uri)) {
+ return content_provider.uri_template.with({ query: document_uri.fsPath })
+ }
+ else undefined
+}
+
+function decode_preview(preview_uri: Uri | undefined): Uri | undefined
+{
+ if (preview_uri && preview_uri.scheme === content_provider.uri_scheme) {
+ return Uri.file(preview_uri.query)
+ }
+ else undefined
+}
+
+
+/* setup */
+
+let language_client: LanguageClient
+
+export function setup(context: ExtensionContext, client: LanguageClient)
+{
+ context.subscriptions.push(content_provider.register())
+
+ language_client = client
+ language_client.onNotification(protocol.preview_response_type, params =>
+ {
+ const preview_uri = encode_preview(Uri.parse(params.uri))
+ if (preview_uri) {
+ content_provider.set_content(preview_uri, params.content)
+ content_provider.update(preview_uri)
+
+ const existing_document =
+ workspace.textDocuments.find(document =>
+ document.uri.scheme === preview_uri.scheme &&
+ document.uri.query === preview_uri.query)
+ if (!existing_document && params.column != 0) {
+ commands.executeCommand("vscode.previewHtml", preview_uri, params.column, params.label)
+ }
+ }
+ })
+}
+
+
+/* commands */
+
+export function request(uri?: Uri, split: boolean = false)
+{
+ const document_uri = uri || window.activeTextEditor.document.uri
+ const preview_uri = encode_preview(document_uri)
+ if (preview_uri && language_client) {
+ language_client.sendNotification(protocol.preview_request_type,
+ { uri: document_uri.toString(),
+ column: library.adjacent_editor_column(window.activeTextEditor, split) })
+ }
+}
+
+export function update(preview_uri: Uri)
+{
+ const document_uri = decode_preview(preview_uri)
+ if (document_uri && language_client) {
+ language_client.sendNotification(protocol.preview_request_type,
+ { uri: document_uri.toString(), column: 0 })
+ }
+}
+
+export function source(preview_uri: Uri)
+{
+ const document_uri = decode_preview(preview_uri)
+ if (document_uri) {
+ const editor =
+ window.visibleTextEditors.find(editor =>
+ library.is_file(editor.document.uri) &&
+ editor.document.uri.fsPath === document_uri.fsPath)
+ if (editor) window.showTextDocument(editor.document, editor.viewColumn)
+ else workspace.openTextDocument(document_uri).then(window.showTextDocument)
+ }
+ else commands.executeCommand("workbench.action.navigateBack")
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/src/state_panel.ts Tue Jun 27 23:21:30 2017 +0200
@@ -0,0 +1,78 @@
+'use strict';
+
+import * as library from './library'
+import * as protocol from './protocol'
+import { Content_Provider } from './content_provider'
+import { LanguageClient } from 'vscode-languageclient';
+import { Uri, ExtensionContext, workspace, commands, window } from 'vscode'
+
+
+/* HTML content */
+
+const content_provider = new Content_Provider("isabelle-state")
+
+function encode_state(id: number | undefined): Uri | undefined
+{
+ return id ? content_provider.uri_template.with({ fragment: id.toString() }) : undefined
+}
+
+function decode_state(uri: Uri | undefined): number | undefined
+{
+ if (uri && uri.scheme === content_provider.uri_scheme) {
+ const id = parseInt(uri.fragment)
+ return id ? id : undefined
+ }
+ else undefined
+}
+
+
+/* setup */
+
+let language_client: LanguageClient
+
+export function setup(context: ExtensionContext, client: LanguageClient)
+{
+ context.subscriptions.push(content_provider.register())
+
+ language_client = client
+ language_client.onNotification(protocol.state_output_type, params =>
+ {
+ const uri = encode_state(params.id)
+ if (uri) {
+ content_provider.set_content(uri, params.content)
+ content_provider.update(uri)
+
+ const existing_document =
+ workspace.textDocuments.find(document =>
+ document.uri.scheme === uri.scheme &&
+ document.uri.fragment === uri.fragment)
+ if (!existing_document) {
+ const column = library.adjacent_editor_column(window.activeTextEditor, true)
+ commands.executeCommand("vscode.previewHtml", uri, column, "State")
+ }
+ }
+ })
+}
+
+
+/* commands */
+
+export function init(uri: Uri)
+{
+ if (language_client) language_client.sendNotification(protocol.state_init_type)
+}
+
+export function exit(id: number)
+{
+ if (language_client) language_client.sendNotification(protocol.state_exit_type, { id: id })
+}
+
+export function locate(id: number)
+{
+ if (language_client) language_client.sendNotification(protocol.state_locate_type, { id: id })
+}
+
+export function update(id: number)
+{
+ if (language_client) language_client.sendNotification(protocol.state_update_type, { id: id })
+}
--- a/src/Tools/VSCode/src/state_panel.scala Tue Jun 27 15:10:13 2017 +0100
+++ b/src/Tools/VSCode/src/state_panel.scala Tue Jun 27 23:21:30 2017 +0200
@@ -62,9 +62,7 @@
HTML.output_document(
List(HTML.style(HTML.fonts_css()),
HTML.style_file(Url.print_file(HTML.isabelle_css.file))),
- List(
- HTML.chapter("Proof state"),
- HTML.source(text)),
+ List(controls, HTML.source(text)),
css = "")
output(content)
})
@@ -93,6 +91,34 @@
def auto_update() { if (auto_update_enabled.value) update() }
+ /* controls */
+
+ private def id_parameter: XML.Elem =
+ HTML.GUI.parameter(id.toString, name = "id")
+
+ private def auto_update_button: XML.Elem =
+ HTML.GUI.checkbox(HTML.text("Auto update"),
+ name = "auto_update",
+ tooltip = "Indicate automatic update following cursor movement",
+ submit = true,
+ selected = auto_update_enabled.value)
+
+ private def update_button: XML.Elem =
+ HTML.GUI.button(List(HTML.bold(HTML.text("Update"))),
+ name = "update",
+ tooltip = "Update display according to the command at cursor position",
+ submit = true)
+
+ private def locate_button: XML.Elem =
+ HTML.GUI.button(HTML.text("Locate"),
+ name = "locate",
+ tooltip = "Locate printed command within source text",
+ submit = true)
+
+ private val controls: XML.Elem =
+ HTML.Wrap_Panel(List(id_parameter, auto_update_button, update_button, locate_button))
+
+
/* main */
private val main =
--- a/src/Tools/jEdit/src/debugger_dockable.scala Tue Jun 27 15:10:13 2017 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala Tue Jun 27 23:21:30 2017 +0200
@@ -284,11 +284,13 @@
private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
private val controls =
- new Wrap_Panel(Wrap_Panel.Alignment.Right)(
- break_button, continue_button, step_button, step_over_button, step_out_button,
- context_label, Component.wrap(context_field),
- expression_label, Component.wrap(expression_field), eval_button, sml_button,
- pretty_text_area.search_label, pretty_text_area.search_field, zoom)
+ Wrap_Panel(
+ List(
+ break_button, continue_button, step_button, step_over_button, step_out_button,
+ context_label, Component.wrap(context_field),
+ expression_label, Component.wrap(expression_field), eval_button, sml_button,
+ pretty_text_area.search_label, pretty_text_area.search_field, zoom))
+
add(controls.peer, BorderLayout.NORTH)
--- a/src/Tools/jEdit/src/document_model.scala Tue Jun 27 15:10:13 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Tue Jun 27 23:21:30 2017 +0200
@@ -301,9 +301,9 @@
{
val preview_root = http_root + "/preview"
val preview =
- HTTP.get(preview_root, uri =>
+ HTTP.get(preview_root, arg =>
for {
- theory <- Library.try_unprefix(preview_root + "/", uri.toString)
+ theory <- Library.try_unprefix(preview_root + "/", arg.uri.toString)
model <-
get_models().iterator.collectFirst(
{ case (node_name, model) if node_name.theory == theory => model })
--- a/src/Tools/jEdit/src/info_dockable.scala Tue Jun 27 15:10:13 2017 +0100
+++ b/src/Tools/jEdit/src/info_dockable.scala Tue Jun 27 23:21:30 2017 +0200
@@ -86,8 +86,9 @@
override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
})
- private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
- pretty_text_area.search_label, pretty_text_area.search_field, zoom)
+ private val controls =
+ Wrap_Panel(List(pretty_text_area.search_label, pretty_text_area.search_field, zoom))
+
add(controls.peer, BorderLayout.NORTH)
--- a/src/Tools/jEdit/src/monitor_dockable.scala Tue Jun 27 15:10:13 2017 +0100
+++ b/src/Tools/jEdit/src/monitor_dockable.scala Tue Jun 27 23:21:30 2017 +0200
@@ -94,8 +94,7 @@
reactions += { case ValueChanged(_) => input_delay.invoke() }
}
- private val controls =
- new Wrap_Panel(Wrap_Panel.Alignment.Right)(ml_stats, select_data, reset_data, limit_data)
+ private val controls = Wrap_Panel(List(ml_stats, select_data, reset_data, limit_data))
/* layout */
--- a/src/Tools/jEdit/src/output_dockable.scala Tue Jun 27 15:10:13 2017 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala Tue Jun 27 23:21:30 2017 +0200
@@ -104,8 +104,10 @@
private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
private val controls =
- new Wrap_Panel(Wrap_Panel.Alignment.Right)(output_state_button, auto_update_button,
- update_button, pretty_text_area.search_label, pretty_text_area.search_field, zoom)
+ Wrap_Panel(
+ List(output_state_button, auto_update_button,
+ update_button, pretty_text_area.search_label, pretty_text_area.search_field, zoom))
+
add(controls.peer, BorderLayout.NORTH)
--- a/src/Tools/jEdit/src/protocol_dockable.scala Tue Jun 27 15:10:13 2017 +0100
+++ b/src/Tools/jEdit/src/protocol_dockable.scala Tue Jun 27 23:21:30 2017 +0200
@@ -22,7 +22,7 @@
private val ml_stats = new Isabelle.ML_Stats
- private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(ml_stats)
+ private val controls = Wrap_Panel(List(ml_stats))
/* text area */
--- a/src/Tools/jEdit/src/query_dockable.scala Tue Jun 27 15:10:13 2017 +0100
+++ b/src/Tools/jEdit/src/query_dockable.scala Tue Jun 27 23:21:30 2017 +0200
@@ -119,10 +119,10 @@
}
private val control_panel =
- new Wrap_Panel(Wrap_Panel.Alignment.Right)(
- query_label, Component.wrap(query), limit, allow_dups,
- process_indicator.component, apply_button,
- pretty_text_area.search_label, pretty_text_area.search_field)
+ Wrap_Panel(
+ List(query_label, Component.wrap(query), limit, allow_dups,
+ process_indicator.component, apply_button,
+ pretty_text_area.search_label, pretty_text_area.search_field))
def select { control_panel.contents += zoom }
@@ -169,9 +169,10 @@
}
private val control_panel =
- new Wrap_Panel(Wrap_Panel.Alignment.Right)(
- query_label, Component.wrap(query), process_indicator.component, apply_button,
- pretty_text_area.search_label, pretty_text_area.search_field)
+ Wrap_Panel(
+ List(
+ query_label, Component.wrap(query), process_indicator.component, apply_button,
+ pretty_text_area.search_label, pretty_text_area.search_field))
def select { control_panel.contents += zoom }
@@ -255,7 +256,7 @@
}
}
- private val control_panel = new Wrap_Panel(Wrap_Panel.Alignment.Right)()
+ private val control_panel = Wrap_Panel()
def select
{
--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala Tue Jun 27 15:10:13 2017 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala Tue Jun 27 23:21:30 2017 +0200
@@ -153,37 +153,38 @@
/* controls */
- private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
- new CheckBox("Auto update") {
- selected = do_update
- reactions += {
- case ButtonClicked(_) =>
- do_update = this.selected
- handle_update(do_update)
- }
- },
- new Button("Update") {
- reactions += {
- case ButtonClicked(_) =>
- handle_update(true)
- }
- },
- new Separator(Orientation.Vertical),
- new Button("Show trace") {
- reactions += {
- case ButtonClicked(_) =>
- show_trace()
- }
- },
- new Button("Clear memory") {
- reactions += {
- case ButtonClicked(_) =>
- Simplifier_Trace.clear_memory()
- }
- }
- )
+ private val controls =
+ Wrap_Panel(
+ List(
+ new CheckBox("Auto update") {
+ selected = do_update
+ reactions += {
+ case ButtonClicked(_) =>
+ do_update = this.selected
+ handle_update(do_update)
+ }
+ },
+ new Button("Update") {
+ reactions += {
+ case ButtonClicked(_) =>
+ handle_update(true)
+ }
+ },
+ new Separator(Orientation.Vertical),
+ new Button("Show trace") {
+ reactions += {
+ case ButtonClicked(_) =>
+ show_trace()
+ }
+ },
+ new Button("Clear memory") {
+ reactions += {
+ case ButtonClicked(_) =>
+ Simplifier_Trace.clear_memory()
+ }
+ }))
- private val answers = new Wrap_Panel(Wrap_Panel.Alignment.Left)()
+ private val answers = Wrap_Panel(Nil, Wrap_Panel.Alignment.Left)
add(controls.peer, BorderLayout.NORTH)
add(answers.peer, BorderLayout.SOUTH)
--- a/src/Tools/jEdit/src/simplifier_trace_window.scala Tue Jun 27 15:10:13 2017 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala Tue Jun 27 23:21:30 2017 +0200
@@ -192,10 +192,8 @@
/* controls */
- private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
- pretty_text_area.search_label,
- pretty_text_area.search_field,
- zoom)
+ private val controls =
+ Wrap_Panel(List(pretty_text_area.search_label, pretty_text_area.search_field, zoom))
peer.add(controls.peer, BorderLayout.NORTH)
}
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Tue Jun 27 15:10:13 2017 +0100
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Tue Jun 27 23:21:30 2017 +0200
@@ -137,9 +137,10 @@
private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
private val controls =
- new Wrap_Panel(Wrap_Panel.Alignment.Right)(
- provers_label, Component.wrap(provers), isar_proofs, try0,
- process_indicator.component, apply_query, cancel_query, locate_query, zoom)
+ Wrap_Panel(
+ List(provers_label, Component.wrap(provers), isar_proofs, try0,
+ process_indicator.component, apply_query, cancel_query, locate_query, zoom))
+
add(controls.peer, BorderLayout.NORTH)
override def focusOnDefaultComponent { provers.requestFocus }
--- a/src/Tools/jEdit/src/state_dockable.scala Tue Jun 27 15:10:13 2017 +0100
+++ b/src/Tools/jEdit/src/state_dockable.scala Tue Jun 27 23:21:30 2017 +0200
@@ -104,8 +104,10 @@
private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
private val controls =
- new Wrap_Panel(Wrap_Panel.Alignment.Right)(auto_update_button, update_button,
- locate_button, pretty_text_area.search_label, pretty_text_area.search_field, zoom)
+ Wrap_Panel(
+ List(auto_update_button, update_button,
+ locate_button, pretty_text_area.search_label, pretty_text_area.search_field, zoom))
+
add(controls.peer, BorderLayout.NORTH)
--- a/src/Tools/jEdit/src/symbols_dockable.scala Tue Jun 27 15:10:13 2017 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala Tue Jun 27 23:21:30 2017 +0200
@@ -47,7 +47,7 @@
tooltip = GUI.tooltip_lines(cat_lines(txt :: abbrs.map(a => "abbrev: " + a)))
}
- private class Abbrevs_Panel extends Wrap_Panel
+ private class Abbrevs_Panel extends Wrap_Panel(Nil, Wrap_Panel.Alignment.Center)
{
private var abbrevs: Thy_Header.Abbrevs = Nil
@@ -122,7 +122,7 @@
private class Search_Panel extends BorderPanel {
val search_field = new TextField(10)
- val results_panel = new Wrap_Panel
+ val results_panel = Wrap_Panel(Nil, Wrap_Panel.Alignment.Center)
layout(search_field) = BorderPanel.Position.North
layout(new ScrollPane(results_panel)) = BorderPanel.Position.Center
@@ -155,12 +155,12 @@
pages ++=
Symbol.groups.map({ case (group, symbols) =>
+ val control = group == "control"
new TabbedPane.Page(group,
- new ScrollPane(new Wrap_Panel {
- val control = group == "control"
- contents ++= symbols.map(new Symbol_Component(_, control))
- if (control) contents += new Reset_Component
- }), null)
+ new ScrollPane(Wrap_Panel(
+ symbols.map(new Symbol_Component(_, control)) :::
+ (if (control) List(new Reset_Component) else Nil),
+ Wrap_Panel.Alignment.Center)), null)
})
val search_panel = new Search_Panel
--- a/src/Tools/jEdit/src/theories_dockable.scala Tue Jun 27 15:10:13 2017 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala Tue Jun 27 23:21:30 2017 +0200
@@ -85,7 +85,8 @@
private val logic = JEdit_Sessions.logic_selector(PIDE.options.value, true)
private val controls =
- new Wrap_Panel(Wrap_Panel.Alignment.Right)(purge, continuous_checking, session_phase, logic)
+ Wrap_Panel(List(purge, continuous_checking, session_phase, logic))
+
add(controls.peer, BorderLayout.NORTH)
--- a/src/Tools/jEdit/src/timing_dockable.scala Tue Jun 27 15:10:13 2017 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala Tue Jun 27 23:21:30 2017 +0200
@@ -142,8 +142,8 @@
s match { case Value.Double(x) => x >= 0.0 case _ => false })
}
- private val controls =
- new Wrap_Panel(Wrap_Panel.Alignment.Right)(threshold_label, threshold_value)
+ private val controls = Wrap_Panel(List(threshold_label, threshold_value))
+
add(controls.peer, BorderLayout.NORTH)