merged
authorwenzelm
Mon May 19 16:14:08 2014 +0200 (2014-05-19)
changeset 57001db2e51a80ab5
parent 56996 891e992e510f
parent 57000 c914618feef8
child 57002 97a80d41a5ba
merged
     1.1 --- a/Admin/isatest/isatest-makedist	Mon May 19 14:26:58 2014 +0200
     1.2 +++ b/Admin/isatest/isatest-makedist	Mon May 19 16:14:08 2014 +0200
     1.3 @@ -15,6 +15,8 @@
     1.4  
     1.5  SSH="ssh -f"
     1.6  
     1.7 +export THIS_IS_ISATEST_MAKEDIST=true
     1.8 +
     1.9  
    1.10  ## diagnostics
    1.11  
     2.1 --- a/src/Pure/Isar/token.scala	Mon May 19 14:26:58 2014 +0200
     2.2 +++ b/src/Pure/Isar/token.scala	Mon May 19 16:14:08 2014 +0200
     2.3 @@ -173,7 +173,7 @@
     2.4      kind == Token.Kind.STRING ||
     2.5      kind == Token.Kind.NAT
     2.6    def is_xname: Boolean = is_name || kind == Token.Kind.LONG_IDENT
     2.7 -  def is_text: Boolean = is_xname || kind == Token.Kind.VERBATIM
     2.8 +  def is_text: Boolean = is_xname || kind == Token.Kind.VERBATIM || kind == Token.Kind.CARTOUCHE
     2.9    def is_space: Boolean = kind == Token.Kind.SPACE
    2.10    def is_comment: Boolean = kind == Token.Kind.COMMENT
    2.11    def is_improper: Boolean = is_space || is_comment
     3.1 --- a/src/Tools/jEdit/src/active.scala	Mon May 19 14:26:58 2014 +0200
     3.2 +++ b/src/Tools/jEdit/src/active.scala	Mon May 19 16:14:08 2014 +0200
     3.3 @@ -58,6 +58,7 @@
     3.4                        Isabelle.insert_line_padding(text_area, text)
     3.5                      else text_area.setSelectedText(text)
     3.6                  }
     3.7 +                text_area.requestFocus
     3.8  
     3.9                case Simplifier_Trace.Active(serial, answer) =>
    3.10                  Simplifier_Trace.send_reply(PIDE.session, serial, answer)
     4.1 --- a/src/Tools/jEdit/src/query_dockable.scala	Mon May 19 14:26:58 2014 +0200
     4.2 +++ b/src/Tools/jEdit/src/query_dockable.scala	Mon May 19 16:14:08 2014 +0200
     4.3 @@ -251,7 +251,13 @@
     4.4  
     4.5      private val apply_button = new Button("<html><b>Apply</b></html>") {
     4.6        tooltip = "Apply to current context"
     4.7 -      reactions += { case ButtonClicked(_) => apply_query() }
     4.8 +      listenTo(keys)
     4.9 +      reactions += {
    4.10 +        case ButtonClicked(_) => apply_query()
    4.11 +        case evt @ KeyPressed(_, Key.Enter, 0, _) =>
    4.12 +          evt.peer.consume
    4.13 +          apply_query()
    4.14 +      }
    4.15      }
    4.16  
    4.17      private val control_panel = new Wrap_Panel(Wrap_Panel.Alignment.Right)()