# HG changeset patch
# User wenzelm
# Date 1512424606 -3600
# Node ID 33683164777991a0ecfe0e4c8ac52634f3a80e46
# Parent  85d10959c2e44242c0db9cd71de7bfe3bda240d1
added action to make antiquoted cartouche;

diff -r 85d10959c2e4 -r 336831647779 src/Pure/General/antiquote.scala
--- a/src/Pure/General/antiquote.scala	Mon Dec 04 22:54:31 2017 +0100
+++ b/src/Pure/General/antiquote.scala	Mon Dec 04 22:56:46 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 85d10959c2e4 -r 336831647779 src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Mon Dec 04 22:54:31 2017 +0100
+++ b/src/Pure/Isar/token.scala	Mon Dec 04 22:56:46 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 85d10959c2e4 -r 336831647779 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Mon Dec 04 22:54:31 2017 +0100
+++ b/src/Pure/PIDE/rendering.scala	Mon Dec 04 22:56:46 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 85d10959c2e4 -r 336831647779 src/Tools/jEdit/src/actions.xml
--- a/src/Tools/jEdit/src/actions.xml	Mon Dec 04 22:54:31 2017 +0100
+++ b/src/Tools/jEdit/src/actions.xml	Mon Dec 04 22:56:46 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);
diff -r 85d10959c2e4 -r 336831647779 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Mon Dec 04 22:54:31 2017 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Mon Dec 04 22:56:46 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 85d10959c2e4 -r 336831647779 src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Mon Dec 04 22:54:31 2017 +0100
+++ b/src/Tools/jEdit/src/jEdit.props	Mon Dec 04 22:56:46 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