--- 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>\<open>argument\<close>. The action
+"isabelle.antiquoted_cartouche" turns an antiquotation with 0 or 1
+arguments into this format.
+
*** HOL ***
--- 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 */
--- 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
+ }
+ }
}
--- 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) &&
--- 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 =
--- 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)
}
--- 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
--- 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);
</CODE>
</ACTION>
+ <ACTION NAME="isabelle.antiquoted_cartouche">
+ <CODE>
+ isabelle.jedit.Isabelle.antiquoted_cartouche(textArea);
+ </CODE>
+ </ACTION>
<ACTION NAME="isabelle.include-word">
<CODE>
isabelle.jedit.Isabelle.update_dictionary(textArea, true, false);
--- 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)
--- 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
}
--- 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
--- 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 =
--- 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 =
{
--- 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