# HG changeset patch # User wenzelm # Date 1498598490 -7200 # Node ID adb9d538f2680f2709e71aeece74297bd56ef711 # Parent 994322c172745fa4950e89b9748599bc8504bdf2# Parent 8d5cb4ea2b7cc76f46b8a180fb3b186a3534fbad merged diff -r 994322c17274 -r adb9d538f268 src/Pure/GUI/wrap_panel.scala --- 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] diff -r 994322c17274 -r adb9d538f268 src/Pure/General/http.scala --- 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 */ diff -r 994322c17274 -r adb9d538f268 src/Pure/Thy/html.scala --- 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 = diff -r 994322c17274 -r adb9d538f268 src/Tools/Graphview/graph_panel.scala --- 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 diff -r 994322c17274 -r adb9d538f268 src/Tools/Graphview/tree_panel.scala --- 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 */ diff -r 994322c17274 -r adb9d538f268 src/Tools/VSCode/extension/package.json --- 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" diff -r 994322c17274 -r adb9d538f268 src/Tools/VSCode/extension/src/preview_panel.ts --- /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") +} diff -r 994322c17274 -r adb9d538f268 src/Tools/VSCode/extension/src/state_panel.ts --- /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 }) +} diff -r 994322c17274 -r adb9d538f268 src/Tools/VSCode/src/state_panel.scala --- 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 = diff -r 994322c17274 -r adb9d538f268 src/Tools/jEdit/src/debugger_dockable.scala --- 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) diff -r 994322c17274 -r adb9d538f268 src/Tools/jEdit/src/document_model.scala --- 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 }) diff -r 994322c17274 -r adb9d538f268 src/Tools/jEdit/src/info_dockable.scala --- 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) diff -r 994322c17274 -r adb9d538f268 src/Tools/jEdit/src/monitor_dockable.scala --- 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 */ diff -r 994322c17274 -r adb9d538f268 src/Tools/jEdit/src/output_dockable.scala --- 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) diff -r 994322c17274 -r adb9d538f268 src/Tools/jEdit/src/protocol_dockable.scala --- 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 */ diff -r 994322c17274 -r adb9d538f268 src/Tools/jEdit/src/query_dockable.scala --- 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 { diff -r 994322c17274 -r adb9d538f268 src/Tools/jEdit/src/simplifier_trace_dockable.scala --- 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) diff -r 994322c17274 -r adb9d538f268 src/Tools/jEdit/src/simplifier_trace_window.scala --- 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) } diff -r 994322c17274 -r adb9d538f268 src/Tools/jEdit/src/sledgehammer_dockable.scala --- 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 } diff -r 994322c17274 -r adb9d538f268 src/Tools/jEdit/src/state_dockable.scala --- 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) diff -r 994322c17274 -r adb9d538f268 src/Tools/jEdit/src/symbols_dockable.scala --- 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 diff -r 994322c17274 -r adb9d538f268 src/Tools/jEdit/src/theories_dockable.scala --- 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) diff -r 994322c17274 -r adb9d538f268 src/Tools/jEdit/src/timing_dockable.scala --- 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)