--- 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
--- 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
--- 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)
--- 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("<html><b>Apply</b></html>") {
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)()