# HG changeset patch # User wenzelm # Date 1512425452 -3600 # Node ID 66ce07e8dbf2e555b894f6738c2acc424ae60aac # Parent 335ed2834ebcdc77266a218f5abf6cf0ee88cf29# Parent 540eeaf88a635696e6617376f500e0524115df71 merged diff -r 335ed2834ebc -r 66ce07e8dbf2 NEWS --- a/NEWS Mon Dec 04 20:24:17 2017 +0100 +++ b/NEWS Mon Dec 04 23:10:52 2017 +0100 @@ -61,6 +61,12 @@ isabelle jedit -d '$AFP' -S Formal_SSA -A HOL isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis +* Named control symbols (without special Unicode rendering) are shown as +bold-italic keyword. This is particularly useful for the short form of +antiquotations with control symbol: \<^name>\argument\. The action +"isabelle.antiquoted_cartouche" turns an antiquotation with 0 or 1 +arguments into this format. + *** HOL *** diff -r 335ed2834ebc -r 66ce07e8dbf2 src/Pure/GUI/gui_thread.scala --- a/src/Pure/GUI/gui_thread.scala Mon Dec 04 20:24:17 2017 +0100 +++ b/src/Pure/GUI/gui_thread.scala Mon Dec 04 23:10:52 2017 +0100 @@ -45,6 +45,16 @@ else SwingUtilities.invokeLater(new Runnable { def run = body }) } + def future[A](body: => A): Future[A] = + { + if (SwingUtilities.isEventDispatchThread()) Future.value(body) + else { + val promise = Future.promise[A] + later { promise.fulfill_result(Exn.capture(body)) } + promise + } + } + /* delayed events */ diff -r 335ed2834ebc -r 66ce07e8dbf2 src/Pure/General/antiquote.scala --- a/src/Pure/General/antiquote.scala Mon Dec 04 20:24:17 2017 +0100 +++ b/src/Pure/General/antiquote.scala Mon Dec 04 23:10:52 2017 +0100 @@ -54,4 +54,12 @@ Position.here(Position.Line(next.pos.line))) } } + + def read_antiq_body(input: CharSequence): Option[String] = + { + read(input) match { + case List(Antiq(source)) => Some(source.substring(2, source.length - 1)) + case _ => None + } + } } diff -r 335ed2834ebc -r 66ce07e8dbf2 src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Mon Dec 04 20:24:17 2017 +0100 +++ b/src/Pure/General/symbol.scala Mon Dec 04 23:10:52 2017 +0100 @@ -563,6 +563,9 @@ def is_open(sym: Symbol): Boolean = sym == open_decoded || sym == open def is_close(sym: Symbol): Boolean = sym == close_decoded || sym == close + def cartouche(s: String): String = open + s + close + def cartouche_decoded(s: String): String = open_decoded + s + close_decoded + /* symbols for symbolic identifiers */ @@ -577,8 +580,14 @@ /* control symbols */ + val control_prefix = "\\<^" + val control_suffix = ">" + + def is_control_encoded(sym: Symbol): Boolean = + sym.startsWith(control_prefix) && sym.endsWith(control_suffix) + def is_control(sym: Symbol): Boolean = - (sym.startsWith("\\<^") && sym.endsWith(">")) || symbols.control_decoded.contains(sym) + is_control_encoded(sym) || symbols.control_decoded.contains(sym) def is_controllable(sym: Symbol): Boolean = !is_blank(sym) && !is_control(sym) && !is_open(sym) && !is_close(sym) && diff -r 335ed2834ebc -r 66ce07e8dbf2 src/Pure/Isar/token.scala --- a/src/Pure/Isar/token.scala Mon Dec 04 20:24:17 2017 +0100 +++ b/src/Pure/Isar/token.scala Mon Dec 04 23:10:52 2017 +0100 @@ -165,6 +165,16 @@ else quote(name.replace("\"", "\\\"")) + /* plain antiquotation (0 or 1 args) */ + + def read_antiq_arg(keywords: Keyword.Keywords, inp: CharSequence): Option[(String, Option[String])] = + explode(keywords, inp).filter(_.is_proper) match { + case List(t) if t.is_name => Some(t.content, None) + case List(t1, t2) if t1.is_name && t2.is_embedded => Some(t1.content, Some(t2.content)) + case _ => None + } + + /* implode */ def implode(toks: List[Token]): String = diff -r 335ed2834ebc -r 66ce07e8dbf2 src/Pure/PIDE/rendering.scala --- a/src/Pure/PIDE/rendering.scala Mon Dec 04 20:24:17 2017 +0100 +++ b/src/Pure/PIDE/rendering.scala Mon Dec 04 23:10:52 2017 +0100 @@ -204,6 +204,8 @@ Markup.BAD) val caret_focus_elements = Markup.Elements(Markup.ENTITY) + + val antiquoted_elements = Markup.Elements(Markup.ANTIQUOTED) } abstract class Rendering( @@ -631,4 +633,13 @@ } } } + + + /* antiquoted text */ + + def antiquoted(range: Text.Range): Option[Text.Range] = + snapshot.cumulate[Option[Text.Range]](range, None, Rendering.antiquoted_elements, _ => + { + case (res, info) => if (res.isEmpty) Some(Some(info.range)) else None + }).headOption.flatMap(_.info) } diff -r 335ed2834ebc -r 66ce07e8dbf2 src/Pure/Tools/update_cartouches.scala --- a/src/Pure/Tools/update_cartouches.scala Mon Dec 04 20:24:17 2017 +0100 +++ b/src/Pure/Tools/update_cartouches.scala Mon Dec 04 23:10:52 2017 +0100 @@ -11,9 +11,6 @@ { /* update cartouches */ - private def cartouche(s: String): String = - Symbol.open + s + Symbol.close - private val Verbatim_Body = """(?s)[ \t]*(.*?)[ \t]*""".r val Text_Antiq = """(?s)@\{\s*text\b\s*(.+)\}""".r @@ -27,7 +24,7 @@ ant match { case Antiquote.Antiq(Text_Antiq(body)) => Token.explode(Keyword.Keywords.empty, body).filterNot(_.is_space) match { - case List(tok) => Antiquote.Control(cartouche(tok.content)) + case List(tok) => Antiquote.Control(Symbol.cartouche(tok.content)) case _ => ant } case _ => ant @@ -45,10 +42,10 @@ val text1 = (for (tok <- Token.explode(Keyword.Keywords.empty, text0).iterator) yield { - if (tok.kind == Token.Kind.ALT_STRING) cartouche(tok.content) + if (tok.kind == Token.Kind.ALT_STRING) Symbol.cartouche(tok.content) else if (tok.kind == Token.Kind.VERBATIM) { tok.content match { - case Verbatim_Body(s) => cartouche(s) + case Verbatim_Body(s) => Symbol.cartouche(s) case s => tok.source } } @@ -68,7 +65,7 @@ if (content == content1) tok.source else if (tok.kind == Token.Kind.STRING) Outer_Syntax.quote_string(content1) - else cartouche(content1) + else Symbol.cartouche(content1) } else tok.source }).mkString diff -r 335ed2834ebc -r 66ce07e8dbf2 src/Tools/jEdit/src/actions.xml --- a/src/Tools/jEdit/src/actions.xml Mon Dec 04 20:24:17 2017 +0100 +++ b/src/Tools/jEdit/src/actions.xml Mon Dec 04 23:10:52 2017 +0100 @@ -117,6 +117,11 @@ isabelle.jedit.Isabelle.input_bsup(textArea); + + + isabelle.jedit.Isabelle.antiquoted_cartouche(textArea); + + isabelle.jedit.Isabelle.update_dictionary(textArea, true, false); diff -r 335ed2834ebc -r 66ce07e8dbf2 src/Tools/jEdit/src/isabelle.scala --- a/src/Tools/jEdit/src/isabelle.scala Mon Dec 04 20:24:17 2017 +0100 +++ b/src/Tools/jEdit/src/isabelle.scala Mon Dec 04 23:10:52 2017 +0100 @@ -420,6 +420,36 @@ { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) } + /* antiquoted cartouche */ + + def antiquoted_cartouche(text_area: TextArea) + { + val buffer = text_area.getBuffer + for { + doc_view <- Document_View.get(text_area) + rendering = doc_view.get_rendering() + caret_range = JEdit_Lib.caret_range(text_area) + antiq_range <- rendering.antiquoted(caret_range) + antiq_text <- JEdit_Lib.get_text(buffer, antiq_range) + body_text <- Antiquote.read_antiq_body(antiq_text) + (name, arg) <- Token.read_antiq_arg(Keyword.Keywords.empty, body_text) + if Symbol.is_ascii_identifier(name) + } { + val op_text = + Isabelle_Encoding.perhaps_decode(buffer, + Symbol.control_prefix + name + Symbol.control_suffix) + val arg_text = + if (arg.isEmpty) "" + else if (Isabelle_Encoding.is_active(buffer)) Symbol.cartouche_decoded(arg.get) + else Symbol.cartouche(arg.get) + + buffer.remove(antiq_range.start, antiq_range.length) + text_area.moveCaretPosition(antiq_range.start) + text_area.setSelectedText(op_text + arg_text) + } + } + + /* spell-checker dictionary */ def update_dictionary(text_area: JEditTextArea, include: Boolean, permanent: Boolean) diff -r 335ed2834ebc -r 66ce07e8dbf2 src/Tools/jEdit/src/isabelle_encoding.scala --- a/src/Tools/jEdit/src/isabelle_encoding.scala Mon Dec 04 20:24:17 2017 +0100 +++ b/src/Tools/jEdit/src/isabelle_encoding.scala Mon Dec 04 23:10:52 2017 +0100 @@ -17,6 +17,6 @@ def is_active(buffer: JEditBuffer): Boolean = buffer.getStringProperty(JEditBuffer.ENCODING).asInstanceOf[String] == "UTF-8-Isabelle" - def maybe_decode(buffer: JEditBuffer, s: String): String = + def perhaps_decode(buffer: JEditBuffer, s: String): String = if (is_active(buffer)) Symbol.decode(s) else s } diff -r 335ed2834ebc -r 66ce07e8dbf2 src/Tools/jEdit/src/jEdit.props --- a/src/Tools/jEdit/src/jEdit.props Mon Dec 04 20:24:17 2017 +0100 +++ b/src/Tools/jEdit/src/jEdit.props Mon Dec 04 23:10:52 2017 +0100 @@ -186,6 +186,7 @@ home.shortcut= insert-newline-indent.shortcut= insert-newline.shortcut= +isabelle.antiquoted_cartouche.label=Make antiquoted cartouche isabelle-debugger.dock-position=floating isabelle-documentation.dock-position=right isabelle-output.dock-position=bottom diff -r 335ed2834ebc -r 66ce07e8dbf2 src/Tools/jEdit/src/symbols_dockable.scala --- a/src/Tools/jEdit/src/symbols_dockable.scala Mon Dec 04 20:24:17 2017 +0100 +++ b/src/Tools/jEdit/src/symbols_dockable.scala Mon Dec 04 23:10:52 2017 +0100 @@ -40,7 +40,7 @@ Action(text) { val text_area = view.getTextArea val (s1, s2) = - Completion.split_template(Isabelle_Encoding.maybe_decode(text_area.getBuffer, txt)) + Completion.split_template(Isabelle_Encoding.perhaps_decode(text_area.getBuffer, txt)) text_area.setSelectedText(s1 + s2) text_area.moveCaretPosition(text_area.getCaretPosition - s2.length) text_area.requestFocus @@ -100,7 +100,7 @@ if (is_control && HTML.is_control(symbol)) Syntax_Style.edit_control_style(text_area, symbol) else - text_area.setSelectedText(Isabelle_Encoding.maybe_decode(text_area.getBuffer, symbol)) + text_area.setSelectedText(Isabelle_Encoding.perhaps_decode(text_area.getBuffer, symbol)) text_area.requestFocus } tooltip = diff -r 335ed2834ebc -r 66ce07e8dbf2 src/Tools/jEdit/src/syntax_style.scala --- a/src/Tools/jEdit/src/syntax_style.scala Mon Dec 04 20:24:17 2017 +0100 +++ b/src/Tools/jEdit/src/syntax_style.scala Mon Dec 04 23:10:52 2017 +0100 @@ -23,7 +23,6 @@ /* extended syntax styles */ private val plain_range: Int = JEditToken.ID_COUNT - private val full_range = 6 * plain_range + 1 private def check_range(i: Int) { require(0 <= i && i < plain_range) } def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte } @@ -31,6 +30,7 @@ def bold(i: Byte): Byte = { check_range(i); (i + 3 * plain_range).toByte } def user_font(idx: Int, i: Byte): Byte = { check_range(i); (i + (4 + idx) * plain_range).toByte } val hidden: Byte = (6 * plain_range).toByte + val control: Byte = (hidden + JEditToken.DIGIT).toByte private def font_style(style: SyntaxStyle, f: Font => Font): SyntaxStyle = new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, f(style.getFont)) @@ -69,7 +69,10 @@ override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] = { - val new_styles = new Array[SyntaxStyle](full_range) + val style0 = styles(0) + val font0 = style0.getFont + + val new_styles = Array.fill[SyntaxStyle](java.lang.Byte.MAX_VALUE)(styles(0)) for (i <- 0 until plain_range) { val style = styles(i) new_styles(i) = style @@ -83,44 +86,62 @@ } new_styles(hidden) = new SyntaxStyle(hidden_color, null, - { val font = styles(0).getFont - GUI.transform_font(new Font(font.getFamily, 0, 1), - AffineTransform.getScaleInstance(1.0, font.getSize.toDouble)) }) + GUI.transform_font(new Font(font0.getFamily, 0, 1), + AffineTransform.getScaleInstance(1.0, font0.getSize.toDouble))) + new_styles(control) = + new SyntaxStyle(style0.getForegroundColor, style0.getBackgroundColor, + { val font_style = + (if (font0.isItalic) 0 else Font.ITALIC) | + (if (font0.isBold) 0 else Font.BOLD) + new Font(font0.getFamily, font_style, font0.getSize) }) new_styles } } + private def control_style(sym: String): Option[Byte => Byte] = + if (sym == Symbol.sub_decoded) Some(subscript(_)) + else if (sym == Symbol.sup_decoded) Some(superscript(_)) + else if (sym == Symbol.bold_decoded) Some(bold(_)) + else None + def extended(text: CharSequence): Map[Text.Offset, Byte => Byte] = { - // FIXME Symbol.bsub_decoded etc. - def control_style(sym: String): Option[Byte => Byte] = - if (sym == Symbol.sub_decoded) Some(subscript(_)) - else if (sym == Symbol.sup_decoded) Some(superscript(_)) - else if (sym == Symbol.bold_decoded) Some(bold(_)) - else None - var result = Map[Text.Offset, Byte => Byte]() def mark(start: Text.Offset, stop: Text.Offset, style: Byte => Byte) { for (i <- start until stop) result += (i -> style) } + var offset = 0 - var control = "" + var control_sym = "" for (sym <- Symbol.iterator(text)) { - if (control_style(sym).isDefined) control = sym - else if (control != "") { + val end_offset = offset + sym.length + + if (control_style(sym).isDefined) control_sym = sym + else if (control_sym != "") { if (Symbol.is_controllable(sym) && !Symbol.fonts.isDefinedAt(sym)) { - mark(offset - control.length, offset, _ => hidden) - mark(offset, offset + sym.length, control_style(control).get) + mark(offset - control_sym.length, offset, _ => hidden) + mark(offset, end_offset, control_style(control_sym).get) } - control = "" + control_sym = "" } + + if (Symbol.is_control_encoded(sym)) { + val a = offset + Symbol.control_prefix.length + val b = end_offset - Symbol.control_suffix.length + mark(offset, a, _ => hidden) + mark(a, b, _ => control) + mark(b, end_offset, _ => hidden) + } + Symbol.lookup_font(sym) match { - case Some(idx) => mark(offset, offset + sym.length, user_font(idx, _)) + case Some(idx) => mark(offset, end_offset, user_font(idx, _)) case _ => } - offset += sym.length + + offset = end_offset } + result } @@ -133,7 +154,7 @@ val buffer = text_area.getBuffer - val control_decoded = Isabelle_Encoding.maybe_decode(buffer, control) + val control_decoded = Isabelle_Encoding.perhaps_decode(buffer, control) def update_style(text: String): String = { diff -r 335ed2834ebc -r 66ce07e8dbf2 src/Tools/jEdit/src/token_markup.scala --- a/src/Tools/jEdit/src/token_markup.scala Mon Dec 04 20:24:17 2017 +0100 +++ b/src/Tools/jEdit/src/token_markup.scala Mon Dec 04 23:10:52 2017 +0100 @@ -271,10 +271,9 @@ var offset = 0 for ((style, token) <- styled_tokens) { val length = token.length - val end_offset = offset + length - if ((offset until end_offset) exists - (i => extended.isDefinedAt(i) || line.charAt(i) == '\t')) { - for (i <- offset until end_offset) { + val offsets = offset until (offset + length) + if (offsets.exists(i => extended.isDefinedAt(i) || line.charAt(i) == '\t')) { + for (i <- offsets) { val style1 = extended.get(i) match { case None => style