# HG changeset patch # User wenzelm # Date 1400508848 -7200 # Node ID db2e51a80ab595fe94d7cde85e8ee11e7db046cd # Parent 891e992e510fd111b2d08a0beb2eba0d52bbb037# Parent c914618feef8e28b3d70e0a35ad1fee78b9fc583 merged diff -r 891e992e510f -r db2e51a80ab5 Admin/isatest/isatest-makedist --- a/Admin/isatest/isatest-makedist Mon May 19 14:26:58 2014 +0200 +++ b/Admin/isatest/isatest-makedist Mon May 19 16:14:08 2014 +0200 @@ -15,6 +15,8 @@ SSH="ssh -f" +export THIS_IS_ISATEST_MAKEDIST=true + ## diagnostics diff -r 891e992e510f -r db2e51a80ab5 src/Pure/Isar/token.scala --- a/src/Pure/Isar/token.scala Mon May 19 14:26:58 2014 +0200 +++ b/src/Pure/Isar/token.scala Mon May 19 16:14:08 2014 +0200 @@ -173,7 +173,7 @@ kind == Token.Kind.STRING || kind == Token.Kind.NAT def is_xname: Boolean = is_name || kind == Token.Kind.LONG_IDENT - def is_text: Boolean = is_xname || kind == Token.Kind.VERBATIM + def is_text: Boolean = is_xname || kind == Token.Kind.VERBATIM || kind == Token.Kind.CARTOUCHE def is_space: Boolean = kind == Token.Kind.SPACE def is_comment: Boolean = kind == Token.Kind.COMMENT def is_improper: Boolean = is_space || is_comment diff -r 891e992e510f -r db2e51a80ab5 src/Tools/jEdit/src/active.scala --- a/src/Tools/jEdit/src/active.scala Mon May 19 14:26:58 2014 +0200 +++ b/src/Tools/jEdit/src/active.scala Mon May 19 16:14:08 2014 +0200 @@ -58,6 +58,7 @@ Isabelle.insert_line_padding(text_area, text) else text_area.setSelectedText(text) } + text_area.requestFocus case Simplifier_Trace.Active(serial, answer) => Simplifier_Trace.send_reply(PIDE.session, serial, answer) diff -r 891e992e510f -r db2e51a80ab5 src/Tools/jEdit/src/query_dockable.scala --- a/src/Tools/jEdit/src/query_dockable.scala Mon May 19 14:26:58 2014 +0200 +++ b/src/Tools/jEdit/src/query_dockable.scala Mon May 19 16:14:08 2014 +0200 @@ -251,7 +251,13 @@ private val apply_button = new Button("Apply") { tooltip = "Apply to current context" - reactions += { case ButtonClicked(_) => apply_query() } + listenTo(keys) + reactions += { + case ButtonClicked(_) => apply_query() + case evt @ KeyPressed(_, Key.Enter, 0, _) => + evt.peer.consume + apply_query() + } } private val control_panel = new Wrap_Panel(Wrap_Panel.Alignment.Right)()