merged
authorwenzelm
Mon Dec 04 23:10:52 2017 +0100 (4 months ago)
changeset 6713466ce07e8dbf2
parent 67124 335ed2834ebc
parent 67133 540eeaf88a63
child 67135 1a94352812f4
child 67136 1368cfa92b7a
merged
     1.1 --- a/NEWS	Mon Dec 04 20:24:17 2017 +0100
     1.2 +++ b/NEWS	Mon Dec 04 23:10:52 2017 +0100
     1.3 @@ -61,6 +61,12 @@
     1.4      isabelle jedit -d '$AFP' -S Formal_SSA -A HOL
     1.5      isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis
     1.6  
     1.7 +* Named control symbols (without special Unicode rendering) are shown as
     1.8 +bold-italic keyword. This is particularly useful for the short form of
     1.9 +antiquotations with control symbol: \<^name>\<open>argument\<close>. The action
    1.10 +"isabelle.antiquoted_cartouche" turns an antiquotation with 0 or 1
    1.11 +arguments into this format.
    1.12 +
    1.13  
    1.14  *** HOL ***
    1.15  
     2.1 --- a/src/Pure/GUI/gui_thread.scala	Mon Dec 04 20:24:17 2017 +0100
     2.2 +++ b/src/Pure/GUI/gui_thread.scala	Mon Dec 04 23:10:52 2017 +0100
     2.3 @@ -45,6 +45,16 @@
     2.4      else SwingUtilities.invokeLater(new Runnable { def run = body })
     2.5    }
     2.6  
     2.7 +  def future[A](body: => A): Future[A] =
     2.8 +  {
     2.9 +    if (SwingUtilities.isEventDispatchThread()) Future.value(body)
    2.10 +    else {
    2.11 +      val promise = Future.promise[A]
    2.12 +      later { promise.fulfill_result(Exn.capture(body)) }
    2.13 +      promise
    2.14 +    }
    2.15 +  }
    2.16 +
    2.17  
    2.18    /* delayed events */
    2.19  
     3.1 --- a/src/Pure/General/antiquote.scala	Mon Dec 04 20:24:17 2017 +0100
     3.2 +++ b/src/Pure/General/antiquote.scala	Mon Dec 04 23:10:52 2017 +0100
     3.3 @@ -54,4 +54,12 @@
     3.4            Position.here(Position.Line(next.pos.line)))
     3.5      }
     3.6    }
     3.7 +
     3.8 +  def read_antiq_body(input: CharSequence): Option[String] =
     3.9 +  {
    3.10 +    read(input) match {
    3.11 +      case List(Antiq(source)) => Some(source.substring(2, source.length - 1))
    3.12 +      case _ => None
    3.13 +    }
    3.14 +  }
    3.15  }
     4.1 --- a/src/Pure/General/symbol.scala	Mon Dec 04 20:24:17 2017 +0100
     4.2 +++ b/src/Pure/General/symbol.scala	Mon Dec 04 23:10:52 2017 +0100
     4.3 @@ -563,6 +563,9 @@
     4.4    def is_open(sym: Symbol): Boolean = sym == open_decoded || sym == open
     4.5    def is_close(sym: Symbol): Boolean = sym == close_decoded || sym == close
     4.6  
     4.7 +  def cartouche(s: String): String = open + s + close
     4.8 +  def cartouche_decoded(s: String): String = open_decoded + s + close_decoded
     4.9 +
    4.10  
    4.11    /* symbols for symbolic identifiers */
    4.12  
    4.13 @@ -577,8 +580,14 @@
    4.14  
    4.15    /* control symbols */
    4.16  
    4.17 +  val control_prefix = "\\<^"
    4.18 +  val control_suffix = ">"
    4.19 +
    4.20 +  def is_control_encoded(sym: Symbol): Boolean =
    4.21 +    sym.startsWith(control_prefix) && sym.endsWith(control_suffix)
    4.22 +
    4.23    def is_control(sym: Symbol): Boolean =
    4.24 -    (sym.startsWith("\\<^") && sym.endsWith(">")) || symbols.control_decoded.contains(sym)
    4.25 +    is_control_encoded(sym) || symbols.control_decoded.contains(sym)
    4.26  
    4.27    def is_controllable(sym: Symbol): Boolean =
    4.28      !is_blank(sym) && !is_control(sym) && !is_open(sym) && !is_close(sym) &&
     5.1 --- a/src/Pure/Isar/token.scala	Mon Dec 04 20:24:17 2017 +0100
     5.2 +++ b/src/Pure/Isar/token.scala	Mon Dec 04 23:10:52 2017 +0100
     5.3 @@ -165,6 +165,16 @@
     5.4      else quote(name.replace("\"", "\\\""))
     5.5  
     5.6  
     5.7 +  /* plain antiquotation (0 or 1 args) */
     5.8 +
     5.9 +  def read_antiq_arg(keywords: Keyword.Keywords, inp: CharSequence): Option[(String, Option[String])] =
    5.10 +    explode(keywords, inp).filter(_.is_proper) match {
    5.11 +      case List(t) if t.is_name => Some(t.content, None)
    5.12 +      case List(t1, t2) if t1.is_name && t2.is_embedded => Some(t1.content, Some(t2.content))
    5.13 +      case _ => None
    5.14 +    }
    5.15 +
    5.16 +
    5.17    /* implode */
    5.18  
    5.19    def implode(toks: List[Token]): String =
     6.1 --- a/src/Pure/PIDE/rendering.scala	Mon Dec 04 20:24:17 2017 +0100
     6.2 +++ b/src/Pure/PIDE/rendering.scala	Mon Dec 04 23:10:52 2017 +0100
     6.3 @@ -204,6 +204,8 @@
     6.4        Markup.BAD)
     6.5  
     6.6    val caret_focus_elements = Markup.Elements(Markup.ENTITY)
     6.7 +
     6.8 +  val antiquoted_elements = Markup.Elements(Markup.ANTIQUOTED)
     6.9  }
    6.10  
    6.11  abstract class Rendering(
    6.12 @@ -631,4 +633,13 @@
    6.13        }
    6.14      }
    6.15    }
    6.16 +
    6.17 +
    6.18 +  /* antiquoted text */
    6.19 +
    6.20 +  def antiquoted(range: Text.Range): Option[Text.Range] =
    6.21 +    snapshot.cumulate[Option[Text.Range]](range, None, Rendering.antiquoted_elements, _ =>
    6.22 +      {
    6.23 +        case (res, info) => if (res.isEmpty) Some(Some(info.range)) else None
    6.24 +      }).headOption.flatMap(_.info)
    6.25  }
     7.1 --- a/src/Pure/Tools/update_cartouches.scala	Mon Dec 04 20:24:17 2017 +0100
     7.2 +++ b/src/Pure/Tools/update_cartouches.scala	Mon Dec 04 23:10:52 2017 +0100
     7.3 @@ -11,9 +11,6 @@
     7.4  {
     7.5    /* update cartouches */
     7.6  
     7.7 -  private def cartouche(s: String): String =
     7.8 -    Symbol.open + s + Symbol.close
     7.9 -
    7.10    private val Verbatim_Body = """(?s)[ \t]*(.*?)[ \t]*""".r
    7.11  
    7.12    val Text_Antiq = """(?s)@\{\s*text\b\s*(.+)\}""".r
    7.13 @@ -27,7 +24,7 @@
    7.14              ant match {
    7.15                case Antiquote.Antiq(Text_Antiq(body)) =>
    7.16                  Token.explode(Keyword.Keywords.empty, body).filterNot(_.is_space) match {
    7.17 -                  case List(tok) => Antiquote.Control(cartouche(tok.content))
    7.18 +                  case List(tok) => Antiquote.Control(Symbol.cartouche(tok.content))
    7.19                    case _ => ant
    7.20                  }
    7.21                case _ => ant
    7.22 @@ -45,10 +42,10 @@
    7.23      val text1 =
    7.24        (for (tok <- Token.explode(Keyword.Keywords.empty, text0).iterator)
    7.25          yield {
    7.26 -          if (tok.kind == Token.Kind.ALT_STRING) cartouche(tok.content)
    7.27 +          if (tok.kind == Token.Kind.ALT_STRING) Symbol.cartouche(tok.content)
    7.28            else if (tok.kind == Token.Kind.VERBATIM) {
    7.29              tok.content match {
    7.30 -              case Verbatim_Body(s) => cartouche(s)
    7.31 +              case Verbatim_Body(s) => Symbol.cartouche(s)
    7.32                case s => tok.source
    7.33              }
    7.34            }
    7.35 @@ -68,7 +65,7 @@
    7.36  
    7.37                if (content == content1) tok.source
    7.38                else if (tok.kind == Token.Kind.STRING) Outer_Syntax.quote_string(content1)
    7.39 -              else cartouche(content1)
    7.40 +              else Symbol.cartouche(content1)
    7.41              }
    7.42              else tok.source
    7.43            }).mkString
     8.1 --- a/src/Tools/jEdit/src/actions.xml	Mon Dec 04 20:24:17 2017 +0100
     8.2 +++ b/src/Tools/jEdit/src/actions.xml	Mon Dec 04 23:10:52 2017 +0100
     8.3 @@ -117,6 +117,11 @@
     8.4  	    isabelle.jedit.Isabelle.input_bsup(textArea);
     8.5  	  </CODE>
     8.6  	</ACTION>
     8.7 +	<ACTION NAME="isabelle.antiquoted_cartouche">
     8.8 +	  <CODE>
     8.9 +	    isabelle.jedit.Isabelle.antiquoted_cartouche(textArea);
    8.10 +	  </CODE>
    8.11 +	</ACTION>
    8.12  	<ACTION NAME="isabelle.include-word">
    8.13  	  <CODE>
    8.14  	    isabelle.jedit.Isabelle.update_dictionary(textArea, true, false);
     9.1 --- a/src/Tools/jEdit/src/isabelle.scala	Mon Dec 04 20:24:17 2017 +0100
     9.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Mon Dec 04 23:10:52 2017 +0100
     9.3 @@ -420,6 +420,36 @@
     9.4    { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) }
     9.5  
     9.6  
     9.7 +  /* antiquoted cartouche */
     9.8 +
     9.9 +  def antiquoted_cartouche(text_area: TextArea)
    9.10 +  {
    9.11 +    val buffer = text_area.getBuffer
    9.12 +    for {
    9.13 +      doc_view <- Document_View.get(text_area)
    9.14 +      rendering = doc_view.get_rendering()
    9.15 +      caret_range = JEdit_Lib.caret_range(text_area)
    9.16 +      antiq_range <- rendering.antiquoted(caret_range)
    9.17 +      antiq_text <- JEdit_Lib.get_text(buffer, antiq_range)
    9.18 +      body_text <- Antiquote.read_antiq_body(antiq_text)
    9.19 +      (name, arg) <- Token.read_antiq_arg(Keyword.Keywords.empty, body_text)
    9.20 +      if Symbol.is_ascii_identifier(name)
    9.21 +    } {
    9.22 +      val op_text =
    9.23 +        Isabelle_Encoding.perhaps_decode(buffer,
    9.24 +          Symbol.control_prefix + name + Symbol.control_suffix)
    9.25 +      val arg_text =
    9.26 +        if (arg.isEmpty) ""
    9.27 +        else if (Isabelle_Encoding.is_active(buffer)) Symbol.cartouche_decoded(arg.get)
    9.28 +        else Symbol.cartouche(arg.get)
    9.29 +
    9.30 +      buffer.remove(antiq_range.start, antiq_range.length)
    9.31 +      text_area.moveCaretPosition(antiq_range.start)
    9.32 +      text_area.setSelectedText(op_text + arg_text)
    9.33 +    }
    9.34 +  }
    9.35 +
    9.36 +
    9.37    /* spell-checker dictionary */
    9.38  
    9.39    def update_dictionary(text_area: JEditTextArea, include: Boolean, permanent: Boolean)
    10.1 --- a/src/Tools/jEdit/src/isabelle_encoding.scala	Mon Dec 04 20:24:17 2017 +0100
    10.2 +++ b/src/Tools/jEdit/src/isabelle_encoding.scala	Mon Dec 04 23:10:52 2017 +0100
    10.3 @@ -17,6 +17,6 @@
    10.4    def is_active(buffer: JEditBuffer): Boolean =
    10.5      buffer.getStringProperty(JEditBuffer.ENCODING).asInstanceOf[String] == "UTF-8-Isabelle"
    10.6  
    10.7 -  def maybe_decode(buffer: JEditBuffer, s: String): String =
    10.8 +  def perhaps_decode(buffer: JEditBuffer, s: String): String =
    10.9      if (is_active(buffer)) Symbol.decode(s) else s
   10.10  }
    11.1 --- a/src/Tools/jEdit/src/jEdit.props	Mon Dec 04 20:24:17 2017 +0100
    11.2 +++ b/src/Tools/jEdit/src/jEdit.props	Mon Dec 04 23:10:52 2017 +0100
    11.3 @@ -186,6 +186,7 @@
    11.4  home.shortcut=
    11.5  insert-newline-indent.shortcut=
    11.6  insert-newline.shortcut=
    11.7 +isabelle.antiquoted_cartouche.label=Make antiquoted cartouche
    11.8  isabelle-debugger.dock-position=floating
    11.9  isabelle-documentation.dock-position=right
   11.10  isabelle-output.dock-position=bottom
    12.1 --- a/src/Tools/jEdit/src/symbols_dockable.scala	Mon Dec 04 20:24:17 2017 +0100
    12.2 +++ b/src/Tools/jEdit/src/symbols_dockable.scala	Mon Dec 04 23:10:52 2017 +0100
    12.3 @@ -40,7 +40,7 @@
    12.4        Action(text) {
    12.5          val text_area = view.getTextArea
    12.6          val (s1, s2) =
    12.7 -          Completion.split_template(Isabelle_Encoding.maybe_decode(text_area.getBuffer, txt))
    12.8 +          Completion.split_template(Isabelle_Encoding.perhaps_decode(text_area.getBuffer, txt))
    12.9          text_area.setSelectedText(s1 + s2)
   12.10          text_area.moveCaretPosition(text_area.getCaretPosition - s2.length)
   12.11          text_area.requestFocus
   12.12 @@ -100,7 +100,7 @@
   12.13          if (is_control && HTML.is_control(symbol))
   12.14            Syntax_Style.edit_control_style(text_area, symbol)
   12.15          else
   12.16 -          text_area.setSelectedText(Isabelle_Encoding.maybe_decode(text_area.getBuffer, symbol))
   12.17 +          text_area.setSelectedText(Isabelle_Encoding.perhaps_decode(text_area.getBuffer, symbol))
   12.18          text_area.requestFocus
   12.19        }
   12.20      tooltip =
    13.1 --- a/src/Tools/jEdit/src/syntax_style.scala	Mon Dec 04 20:24:17 2017 +0100
    13.2 +++ b/src/Tools/jEdit/src/syntax_style.scala	Mon Dec 04 23:10:52 2017 +0100
    13.3 @@ -23,7 +23,6 @@
    13.4    /* extended syntax styles */
    13.5  
    13.6    private val plain_range: Int = JEditToken.ID_COUNT
    13.7 -  private val full_range = 6 * plain_range + 1
    13.8    private def check_range(i: Int) { require(0 <= i && i < plain_range) }
    13.9  
   13.10    def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
   13.11 @@ -31,6 +30,7 @@
   13.12    def bold(i: Byte): Byte = { check_range(i); (i + 3 * plain_range).toByte }
   13.13    def user_font(idx: Int, i: Byte): Byte = { check_range(i); (i + (4 + idx) * plain_range).toByte }
   13.14    val hidden: Byte = (6 * plain_range).toByte
   13.15 +  val control: Byte = (hidden + JEditToken.DIGIT).toByte
   13.16  
   13.17    private def font_style(style: SyntaxStyle, f: Font => Font): SyntaxStyle =
   13.18      new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, f(style.getFont))
   13.19 @@ -69,7 +69,10 @@
   13.20  
   13.21      override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
   13.22      {
   13.23 -      val new_styles = new Array[SyntaxStyle](full_range)
   13.24 +      val style0 = styles(0)
   13.25 +      val font0 = style0.getFont
   13.26 +
   13.27 +      val new_styles = Array.fill[SyntaxStyle](java.lang.Byte.MAX_VALUE)(styles(0))
   13.28        for (i <- 0 until plain_range) {
   13.29          val style = styles(i)
   13.30          new_styles(i) = style
   13.31 @@ -83,44 +86,62 @@
   13.32        }
   13.33        new_styles(hidden) =
   13.34          new SyntaxStyle(hidden_color, null,
   13.35 -          { val font = styles(0).getFont
   13.36 -            GUI.transform_font(new Font(font.getFamily, 0, 1),
   13.37 -              AffineTransform.getScaleInstance(1.0, font.getSize.toDouble)) })
   13.38 +          GUI.transform_font(new Font(font0.getFamily, 0, 1),
   13.39 +            AffineTransform.getScaleInstance(1.0, font0.getSize.toDouble)))
   13.40 +      new_styles(control) =
   13.41 +        new SyntaxStyle(style0.getForegroundColor, style0.getBackgroundColor,
   13.42 +          { val font_style =
   13.43 +              (if (font0.isItalic) 0 else Font.ITALIC) |
   13.44 +              (if (font0.isBold) 0 else Font.BOLD)
   13.45 +            new Font(font0.getFamily, font_style, font0.getSize) })
   13.46        new_styles
   13.47      }
   13.48    }
   13.49  
   13.50 +  private def control_style(sym: String): Option[Byte => Byte] =
   13.51 +    if (sym == Symbol.sub_decoded) Some(subscript(_))
   13.52 +    else if (sym == Symbol.sup_decoded) Some(superscript(_))
   13.53 +    else if (sym == Symbol.bold_decoded) Some(bold(_))
   13.54 +    else None
   13.55 +
   13.56    def extended(text: CharSequence): Map[Text.Offset, Byte => Byte] =
   13.57    {
   13.58 -    // FIXME Symbol.bsub_decoded etc.
   13.59 -    def control_style(sym: String): Option[Byte => Byte] =
   13.60 -      if (sym == Symbol.sub_decoded) Some(subscript(_))
   13.61 -      else if (sym == Symbol.sup_decoded) Some(superscript(_))
   13.62 -      else if (sym == Symbol.bold_decoded) Some(bold(_))
   13.63 -      else None
   13.64 -
   13.65      var result = Map[Text.Offset, Byte => Byte]()
   13.66      def mark(start: Text.Offset, stop: Text.Offset, style: Byte => Byte)
   13.67      {
   13.68        for (i <- start until stop) result += (i -> style)
   13.69      }
   13.70 +
   13.71      var offset = 0
   13.72 -    var control = ""
   13.73 +    var control_sym = ""
   13.74      for (sym <- Symbol.iterator(text)) {
   13.75 -      if (control_style(sym).isDefined) control = sym
   13.76 -      else if (control != "") {
   13.77 +      val end_offset = offset + sym.length
   13.78 +
   13.79 +      if (control_style(sym).isDefined) control_sym = sym
   13.80 +      else if (control_sym != "") {
   13.81          if (Symbol.is_controllable(sym) && !Symbol.fonts.isDefinedAt(sym)) {
   13.82 -          mark(offset - control.length, offset, _ => hidden)
   13.83 -          mark(offset, offset + sym.length, control_style(control).get)
   13.84 +          mark(offset - control_sym.length, offset, _ => hidden)
   13.85 +          mark(offset, end_offset, control_style(control_sym).get)
   13.86          }
   13.87 -        control = ""
   13.88 +        control_sym = ""
   13.89        }
   13.90 +
   13.91 +      if (Symbol.is_control_encoded(sym)) {
   13.92 +        val a = offset + Symbol.control_prefix.length
   13.93 +        val b = end_offset - Symbol.control_suffix.length
   13.94 +        mark(offset, a, _ => hidden)
   13.95 +        mark(a, b, _ => control)
   13.96 +        mark(b, end_offset, _ => hidden)
   13.97 +      }
   13.98 +
   13.99        Symbol.lookup_font(sym) match {
  13.100 -        case Some(idx) => mark(offset, offset + sym.length, user_font(idx, _))
  13.101 +        case Some(idx) => mark(offset, end_offset, user_font(idx, _))
  13.102          case _ =>
  13.103        }
  13.104 -      offset += sym.length
  13.105 +
  13.106 +      offset = end_offset
  13.107      }
  13.108 +
  13.109      result
  13.110    }
  13.111  
  13.112 @@ -133,7 +154,7 @@
  13.113  
  13.114      val buffer = text_area.getBuffer
  13.115  
  13.116 -    val control_decoded = Isabelle_Encoding.maybe_decode(buffer, control)
  13.117 +    val control_decoded = Isabelle_Encoding.perhaps_decode(buffer, control)
  13.118  
  13.119      def update_style(text: String): String =
  13.120      {
    14.1 --- a/src/Tools/jEdit/src/token_markup.scala	Mon Dec 04 20:24:17 2017 +0100
    14.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Mon Dec 04 23:10:52 2017 +0100
    14.3 @@ -271,10 +271,9 @@
    14.4          var offset = 0
    14.5          for ((style, token) <- styled_tokens) {
    14.6            val length = token.length
    14.7 -          val end_offset = offset + length
    14.8 -          if ((offset until end_offset) exists
    14.9 -              (i => extended.isDefinedAt(i) || line.charAt(i) == '\t')) {
   14.10 -            for (i <- offset until end_offset) {
   14.11 +          val offsets = offset until (offset + length)
   14.12 +          if (offsets.exists(i => extended.isDefinedAt(i) || line.charAt(i) == '\t')) {
   14.13 +            for (i <- offsets) {
   14.14                val style1 =
   14.15                  extended.get(i) match {
   14.16                    case None => style