added action to make antiquoted cartouche;
authorwenzelm
Mon Dec 04 22:56:46 2017 +0100 (4 months ago)
changeset 67132336831647779
parent 67131 85d10959c2e4
child 67133 540eeaf88a63
added action to make antiquoted cartouche;
src/Pure/General/antiquote.scala
src/Pure/Isar/token.scala
src/Pure/PIDE/rendering.scala
src/Tools/jEdit/src/actions.xml
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/jEdit.props
     1.1 --- a/src/Pure/General/antiquote.scala	Mon Dec 04 22:54:31 2017 +0100
     1.2 +++ b/src/Pure/General/antiquote.scala	Mon Dec 04 22:56:46 2017 +0100
     1.3 @@ -54,4 +54,12 @@
     1.4            Position.here(Position.Line(next.pos.line)))
     1.5      }
     1.6    }
     1.7 +
     1.8 +  def read_antiq_body(input: CharSequence): Option[String] =
     1.9 +  {
    1.10 +    read(input) match {
    1.11 +      case List(Antiq(source)) => Some(source.substring(2, source.length - 1))
    1.12 +      case _ => None
    1.13 +    }
    1.14 +  }
    1.15  }
     2.1 --- a/src/Pure/Isar/token.scala	Mon Dec 04 22:54:31 2017 +0100
     2.2 +++ b/src/Pure/Isar/token.scala	Mon Dec 04 22:56:46 2017 +0100
     2.3 @@ -165,6 +165,16 @@
     2.4      else quote(name.replace("\"", "\\\""))
     2.5  
     2.6  
     2.7 +  /* plain antiquotation (0 or 1 args) */
     2.8 +
     2.9 +  def read_antiq_arg(keywords: Keyword.Keywords, inp: CharSequence): Option[(String, Option[String])] =
    2.10 +    explode(keywords, inp).filter(_.is_proper) match {
    2.11 +      case List(t) if t.is_name => Some(t.content, None)
    2.12 +      case List(t1, t2) if t1.is_name && t2.is_embedded => Some(t1.content, Some(t2.content))
    2.13 +      case _ => None
    2.14 +    }
    2.15 +
    2.16 +
    2.17    /* implode */
    2.18  
    2.19    def implode(toks: List[Token]): String =
     3.1 --- a/src/Pure/PIDE/rendering.scala	Mon Dec 04 22:54:31 2017 +0100
     3.2 +++ b/src/Pure/PIDE/rendering.scala	Mon Dec 04 22:56:46 2017 +0100
     3.3 @@ -204,6 +204,8 @@
     3.4        Markup.BAD)
     3.5  
     3.6    val caret_focus_elements = Markup.Elements(Markup.ENTITY)
     3.7 +
     3.8 +  val antiquoted_elements = Markup.Elements(Markup.ANTIQUOTED)
     3.9  }
    3.10  
    3.11  abstract class Rendering(
    3.12 @@ -631,4 +633,13 @@
    3.13        }
    3.14      }
    3.15    }
    3.16 +
    3.17 +
    3.18 +  /* antiquoted text */
    3.19 +
    3.20 +  def antiquoted(range: Text.Range): Option[Text.Range] =
    3.21 +    snapshot.cumulate[Option[Text.Range]](range, None, Rendering.antiquoted_elements, _ =>
    3.22 +      {
    3.23 +        case (res, info) => if (res.isEmpty) Some(Some(info.range)) else None
    3.24 +      }).headOption.flatMap(_.info)
    3.25  }
     4.1 --- a/src/Tools/jEdit/src/actions.xml	Mon Dec 04 22:54:31 2017 +0100
     4.2 +++ b/src/Tools/jEdit/src/actions.xml	Mon Dec 04 22:56:46 2017 +0100
     4.3 @@ -117,6 +117,11 @@
     4.4  	    isabelle.jedit.Isabelle.input_bsup(textArea);
     4.5  	  </CODE>
     4.6  	</ACTION>
     4.7 +	<ACTION NAME="isabelle.antiquoted_cartouche">
     4.8 +	  <CODE>
     4.9 +	    isabelle.jedit.Isabelle.antiquoted_cartouche(textArea);
    4.10 +	  </CODE>
    4.11 +	</ACTION>
    4.12  	<ACTION NAME="isabelle.include-word">
    4.13  	  <CODE>
    4.14  	    isabelle.jedit.Isabelle.update_dictionary(textArea, true, false);
     5.1 --- a/src/Tools/jEdit/src/isabelle.scala	Mon Dec 04 22:54:31 2017 +0100
     5.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Mon Dec 04 22:56:46 2017 +0100
     5.3 @@ -420,6 +420,36 @@
     5.4    { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) }
     5.5  
     5.6  
     5.7 +  /* antiquoted cartouche */
     5.8 +
     5.9 +  def antiquoted_cartouche(text_area: TextArea)
    5.10 +  {
    5.11 +    val buffer = text_area.getBuffer
    5.12 +    for {
    5.13 +      doc_view <- Document_View.get(text_area)
    5.14 +      rendering = doc_view.get_rendering()
    5.15 +      caret_range = JEdit_Lib.caret_range(text_area)
    5.16 +      antiq_range <- rendering.antiquoted(caret_range)
    5.17 +      antiq_text <- JEdit_Lib.get_text(buffer, antiq_range)
    5.18 +      body_text <- Antiquote.read_antiq_body(antiq_text)
    5.19 +      (name, arg) <- Token.read_antiq_arg(Keyword.Keywords.empty, body_text)
    5.20 +      if Symbol.is_ascii_identifier(name)
    5.21 +    } {
    5.22 +      val op_text =
    5.23 +        Isabelle_Encoding.perhaps_decode(buffer,
    5.24 +          Symbol.control_prefix + name + Symbol.control_suffix)
    5.25 +      val arg_text =
    5.26 +        if (arg.isEmpty) ""
    5.27 +        else if (Isabelle_Encoding.is_active(buffer)) Symbol.cartouche_decoded(arg.get)
    5.28 +        else Symbol.cartouche(arg.get)
    5.29 +
    5.30 +      buffer.remove(antiq_range.start, antiq_range.length)
    5.31 +      text_area.moveCaretPosition(antiq_range.start)
    5.32 +      text_area.setSelectedText(op_text + arg_text)
    5.33 +    }
    5.34 +  }
    5.35 +
    5.36 +
    5.37    /* spell-checker dictionary */
    5.38  
    5.39    def update_dictionary(text_area: JEditTextArea, include: Boolean, permanent: Boolean)
     6.1 --- a/src/Tools/jEdit/src/jEdit.props	Mon Dec 04 22:54:31 2017 +0100
     6.2 +++ b/src/Tools/jEdit/src/jEdit.props	Mon Dec 04 22:56:46 2017 +0100
     6.3 @@ -186,6 +186,7 @@
     6.4  home.shortcut=
     6.5  insert-newline-indent.shortcut=
     6.6  insert-newline.shortcut=
     6.7 +isabelle.antiquoted_cartouche.label=Make antiquoted cartouche
     6.8  isabelle-debugger.dock-position=floating
     6.9  isabelle-documentation.dock-position=right
    6.10  isabelle-output.dock-position=bottom