support for nested text cartouches;
authorwenzelm
Sat Jan 18 19:15:12 2014 +0100 (2014-01-18)
changeset 550338e8243975860
parent 55032 b49366215417
child 55034 04b443d54aee
support for nested text cartouches;
clarified Symbol.is_symbolic: exclude \<open> and \<close>;
etc/isabelle.css
etc/isar-keywords.el
etc/symbols
lib/texinputs/isabelle.sty
lib/texinputs/isabellesym.sty
src/Doc/IsarRef/Inner_Syntax.thy
src/Doc/IsarRef/Outer_Syntax.thy
src/HOL/ROOT
src/HOL/ex/Cartouche_Examples.thy
src/Pure/General/pretty.ML
src/Pure/General/scan.scala
src/Pure/General/symbol.ML
src/Pure/General/symbol.scala
src/Pure/General/symbol_pos.ML
src/Pure/Isar/args.ML
src/Pure/Isar/parse.ML
src/Pure/Isar/token.ML
src/Pure/Isar/token.scala
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/Syntax/lexicon.ML
src/Pure/Thy/html.ML
src/Pure/Thy/latex.ML
src/Pure/Thy/thy_syntax.ML
src/Pure/library.ML
src/Pure/library.scala
src/Pure/pure_thy.ML
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/etc/isabelle.css	Fri Jan 17 20:51:36 2014 +0100
     1.2 +++ b/etc/isabelle.css	Sat Jan 18 19:15:12 2014 +0100
     1.3 @@ -30,6 +30,7 @@
     1.4  .literal        { font-weight: bold; }
     1.5  .delimiter      { }
     1.6  .inner_string   { color: #D2691E; }
     1.7 +.inner_cartouche { color: #CC6600; }
     1.8  .inner_comment  { color: #8B0000; }
     1.9  
    1.10  .bold           { font-weight: bold; }
    1.11 @@ -40,6 +41,7 @@
    1.12  .string         { color: #008B00; }
    1.13  .altstring      { color: #8B8B00; }
    1.14  .verbatim       { color: #00008B; }
    1.15 +.cartouche      { color: #CC6600; }
    1.16  .comment        { color: #8B0000; }
    1.17  .control        { background-color: #FF6A6A; }
    1.18  .bad            { background-color: #FF6A6A; }
     2.1 --- a/etc/isar-keywords.el	Fri Jan 17 20:51:36 2014 +0100
     2.2 +++ b/etc/isar-keywords.el	Sat Jan 18 19:15:12 2014 +0100
     2.3 @@ -38,6 +38,7 @@
     2.4      "bundle"
     2.5      "by"
     2.6      "cannot_undo"
     2.7 +    "cartouche"
     2.8      "case"
     2.9      "case_of_simps"
    2.10      "cd"
    2.11 @@ -389,6 +390,7 @@
    2.12  (defconst isar-keywords-diag
    2.13    '("ML_command"
    2.14      "ML_val"
    2.15 +    "cartouche"
    2.16      "class_deps"
    2.17      "code_deps"
    2.18      "code_thms"
     3.1 --- a/etc/symbols	Fri Jan 17 20:51:36 2014 +0100
     3.2 +++ b/etc/symbols	Sat Jan 18 19:15:12 2014 +0100
     3.3 @@ -348,6 +348,8 @@
     3.4  \<hungarumlaut>         code: 0x0002dd
     3.5  \<some>                 code: 0x0003f5
     3.6  \<newline>              code: 0x0023ce
     3.7 +\<open>                 code: 0x002039  abbrev: <<  font: IsabelleText
     3.8 +\<close>                code: 0x00203a  abbrev: >>  font: IsabelleText
     3.9  \<^sub>                 code: 0x0021e9  group: control  font: IsabelleText
    3.10  \<^sup>                 code: 0x0021e7  group: control  font: IsabelleText
    3.11  \<^bold>                code: 0x002759  group: control  font: IsabelleText
     4.1 --- a/lib/texinputs/isabelle.sty	Fri Jan 17 20:51:36 2014 +0100
     4.2 +++ b/lib/texinputs/isabelle.sty	Sat Jan 18 19:15:12 2014 +0100
     4.3 @@ -97,6 +97,8 @@
     4.4  \chardef\isachartilde=`\~%
     4.5  \def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}%
     4.6  \def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
     4.7 +\def\isacartoucheopen{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
     4.8 +\def\isacartoucheclose{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
     4.9  }
    4.10  
    4.11  
     5.1 --- a/lib/texinputs/isabellesym.sty	Fri Jan 17 20:51:36 2014 +0100
     5.2 +++ b/lib/texinputs/isabellesym.sty	Sat Jan 18 19:15:12 2014 +0100
     5.3 @@ -354,3 +354,6 @@
     5.4  \newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}}
     5.5  \newcommand{\isasymthen}{\isamath{\mathbin{>\!\!\!>}}}
     5.6  \newcommand{\isasymsome}{\isamath{\epsilon\,}}
     5.7 +\newcommand{\isasymopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}
     5.8 +\newcommand{\isasymclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}
     5.9 +
     6.1 --- a/src/Doc/IsarRef/Inner_Syntax.thy	Fri Jan 17 20:51:36 2014 +0100
     6.2 +++ b/src/Doc/IsarRef/Inner_Syntax.thy	Sat Jan 18 19:15:12 2014 +0100
     6.3 @@ -633,14 +633,16 @@
     6.4      @{syntax_def (inner) xnum_token} & = & @{verbatim "#"}@{syntax_ref nat}@{text "  |  "}@{verbatim "#-"}@{syntax_ref nat} \\
     6.5  
     6.6      @{syntax_def (inner) str_token} & = & @{verbatim "''"} @{text "\<dots>"} @{verbatim "''"} \\
     6.7 +    @{syntax_def (inner) cartouche} & = & @{verbatim "\<open>"} @{text "\<dots>"} @{verbatim "\<close>"} \\
     6.8    \end{supertabular}
     6.9    \end{center}
    6.10  
    6.11    The token categories @{syntax (inner) num_token}, @{syntax (inner)
    6.12 -  float_token}, @{syntax (inner) xnum_token}, and @{syntax (inner)
    6.13 -  str_token} are not used in Pure.  Object-logics may implement numerals
    6.14 -  and string constants by adding appropriate syntax declarations,
    6.15 -  together with some translation functions (e.g.\ see Isabelle/HOL).
    6.16 +  float_token}, @{syntax (inner) xnum_token}, @{syntax (inner)
    6.17 +  str_token}, and @{syntax (inner) cartouche} are not used in Pure.
    6.18 +  Object-logics may implement numerals and string literals by adding
    6.19 +  appropriate syntax declarations, together with some translation
    6.20 +  functions (e.g.\ see Isabelle/HOL).
    6.21  
    6.22    The derived categories @{syntax_def (inner) num_const}, @{syntax_def
    6.23    (inner) float_const}, and @{syntax_def (inner) num_const} provide
     7.1 --- a/src/Doc/IsarRef/Outer_Syntax.thy	Fri Jan 17 20:51:36 2014 +0100
     7.2 +++ b/src/Doc/IsarRef/Outer_Syntax.thy	Sat Jan 18 19:15:12 2014 +0100
     7.3 @@ -147,6 +147,7 @@
     7.4      @{syntax_def typevar} & = & @{verbatim "?"}@{text "typefree  |  "}@{verbatim "?"}@{text typefree}@{verbatim "."}@{text nat} \\
     7.5      @{syntax_def string} & = & @{verbatim "\""} @{text "\<dots>"} @{verbatim "\""} \\
     7.6      @{syntax_def altstring} & = & @{verbatim "`"} @{text "\<dots>"} @{verbatim "`"} \\
     7.7 +    @{syntax_def cartouche} & = & @{verbatim "\<open>"} @{text "\<dots>"} @{verbatim "\<close>"} \\
     7.8      @{syntax_def verbatim} & = & @{verbatim "{*"} @{text "\<dots>"} @{verbatim "*"}@{verbatim "}"} \\[1ex]
     7.9  
    7.10      @{text letter} & = & @{text "latin  |  "}@{verbatim "\\"}@{verbatim "<"}@{text latin}@{verbatim ">"}@{text "  |  "}@{verbatim "\\"}@{verbatim "<"}@{text "latin latin"}@{verbatim ">"}@{text "  |  greek  |"} \\
    7.11 @@ -191,6 +192,11 @@
    7.12    text is {\LaTeX} source, one may usually add some blank or comment
    7.13    to avoid the critical character sequence.
    7.14  
    7.15 +  A @{syntax_ref cartouche} consists of arbitrary text, with properly
    7.16 +  balanced blocks of ``@{verbatim "\<open>"}~@{text "\<dots>"}~@{verbatim
    7.17 +  "\<close>"}''.  Note that the rendering of cartouche delimiters is
    7.18 +  usually like this: ``@{text "\<open> \<dots> \<close>"}''.
    7.19 +
    7.20    Source comments take the form @{verbatim "(*"}~@{text
    7.21    "\<dots>"}~@{verbatim "*)"} and may be nested, although the user-interface
    7.22    might prevent this.  Note that this form indicates source comments
     8.1 --- a/src/HOL/ROOT	Fri Jan 17 20:51:36 2014 +0100
     8.2 +++ b/src/HOL/ROOT	Sat Jan 18 19:15:12 2014 +0100
     8.3 @@ -562,6 +562,7 @@
     8.4      SVC_Oracle
     8.5      Simps_Case_Conv_Examples
     8.6      ML
     8.7 +    Cartouche_Examples
     8.8    theories [skip_proofs = false]
     8.9      Meson_Test
    8.10    theories [condition = SVC_HOME]
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/ex/Cartouche_Examples.thy	Sat Jan 18 19:15:12 2014 +0100
     9.3 @@ -0,0 +1,61 @@
     9.4 +header {* Some examples with text cartouches *}
     9.5 +
     9.6 +theory Cartouche_Examples
     9.7 +imports Main
     9.8 +keywords "cartouche" :: diag
     9.9 +begin
    9.10 +
    9.11 +subsection {* Outer syntax *}
    9.12 +
    9.13 +ML {*
    9.14 +  Outer_Syntax.improper_command @{command_spec "cartouche"} ""
    9.15 +    (Parse.cartouche >> (fn s =>
    9.16 +      Toplevel.imperative (fn () => writeln s)))
    9.17 +*}
    9.18 +
    9.19 +cartouche \<open>abc\<close>
    9.20 +cartouche \<open>abc \<open>\<alpha>\<beta>\<gamma>\<close> xzy\<close>
    9.21 +
    9.22 +
    9.23 +subsection {* Inner syntax *}
    9.24 +
    9.25 +syntax "_string_cartouche" :: "cartouche_position \<Rightarrow> string"  ("STR _")
    9.26 +
    9.27 +parse_translation {*
    9.28 +  let
    9.29 +    val mk_nib =
    9.30 +      Syntax.const o Lexicon.mark_const o
    9.31 +        fst o Term.dest_Const o HOLogic.mk_nibble;
    9.32 +
    9.33 +    fun mk_char (s, pos) =
    9.34 +      let
    9.35 +        val c =
    9.36 +          if Symbol.is_ascii s then ord s
    9.37 +          else if s = "" then 10
    9.38 +          else error ("String literal contains illegal symbol: " ^ quote s ^ Position.here pos);
    9.39 +      in Syntax.const @{const_syntax Char} $ mk_nib (c div 16) $ mk_nib (c mod 16) end;
    9.40 +
    9.41 +    fun mk_string [] = Const (@{const_syntax Nil}, @{typ string})
    9.42 +      | mk_string (s :: ss) =
    9.43 +          Syntax.const @{const_syntax Cons} $ mk_char s $ mk_string ss;
    9.44 +
    9.45 +    fun string_tr ctxt args =
    9.46 +      let fun err () = raise TERM ("string_tr", []) in
    9.47 +        (case args of
    9.48 +          [(c as Const (@{syntax_const "_constrain"}, _)) $ Free (s, _) $ p] =>
    9.49 +            (case Term_Position.decode_position p of
    9.50 +              SOME (pos, _) =>
    9.51 +                c $ mk_string (Symbol_Pos.cartouche_content (Symbol_Pos.explode (s, pos))) $ p
    9.52 +            | NONE => err ())
    9.53 +        | _ => err ())
    9.54 +      end;
    9.55 +  in
    9.56 +    [(@{syntax_const "_string_cartouche"}, string_tr)]
    9.57 +  end
    9.58 +*}
    9.59 +
    9.60 +term "STR \<open>\<close>"
    9.61 +term "STR \<open>abc\<close>"
    9.62 +lemma "STR \<open>abc\<close> @ STR \<open>xyz\<close> = STR \<open>abcxyz\<close>" by simp
    9.63 +
    9.64 +end
    10.1 --- a/src/Pure/General/pretty.ML	Fri Jan 17 20:51:36 2014 +0100
    10.2 +++ b/src/Pure/General/pretty.ML	Sat Jan 18 19:15:12 2014 +0100
    10.3 @@ -51,6 +51,7 @@
    10.4    val block_enclose: T * T -> T list -> T
    10.5    val quote: T -> T
    10.6    val backquote: T -> T
    10.7 +  val cartouche: T -> T
    10.8    val separate: string -> T list -> T list
    10.9    val commas: T list -> T list
   10.10    val enclose: string -> string -> T list -> T
   10.11 @@ -182,6 +183,7 @@
   10.12  
   10.13  fun quote prt = blk (1, [str "\"", prt, str "\""]);
   10.14  fun backquote prt = blk (1, [str "`", prt, str "`"]);
   10.15 +fun cartouche prt = blk (1, [str "\\<open>", prt, str "\\<close>"]);
   10.16  
   10.17  fun separate sep prts =
   10.18    flat (Library.separate [str sep, brk 1] (map single prts));
    11.1 --- a/src/Pure/General/scan.scala	Fri Jan 17 20:51:36 2014 +0100
    11.2 +++ b/src/Pure/General/scan.scala	Sat Jan 18 19:15:12 2014 +0100
    11.3 @@ -23,6 +23,7 @@
    11.4    case object Finished extends Context
    11.5    case class Quoted(quote: String) extends Context
    11.6    case object Verbatim extends Context
    11.7 +  case class Cartouche(depth: Int) extends Context
    11.8    case class Comment(depth: Int) extends Context
    11.9  
   11.10  
   11.11 @@ -274,6 +275,72 @@
   11.12        "{*" ~ verbatim_body ^^ { case x ~ y => x + y }
   11.13  
   11.14  
   11.15 +    /* nested text cartouches */
   11.16 +
   11.17 +    private def cartouche_depth(depth: Int): Parser[(String, Int)] = new Parser[(String, Int)]
   11.18 +    {
   11.19 +      require(depth >= 0)
   11.20 +
   11.21 +      def apply(in: Input) =
   11.22 +      {
   11.23 +        val start = in.offset
   11.24 +        val end = in.source.length
   11.25 +        val matcher = new Symbol.Matcher(in.source)
   11.26 +
   11.27 +        var i = start
   11.28 +        var d = depth
   11.29 +        var finished = false
   11.30 +        while (!finished) {
   11.31 +          if (i < end) {
   11.32 +            val n = matcher(i, end)
   11.33 +            val sym = in.source.subSequence(i, i + n).toString
   11.34 +
   11.35 +            if (Symbol.is_open(sym)) { i += n; d += 1 }
   11.36 +            else if (d > 0) {
   11.37 +              i += n
   11.38 +              if (Symbol.is_close(sym)) d -= 1
   11.39 +            }
   11.40 +            else finished = true
   11.41 +          }
   11.42 +          else finished = true
   11.43 +        }
   11.44 +        if (i == start) Failure("bad input", in)
   11.45 +        else Success((in.source.subSequence(start, i).toString, d), in.drop(i - start))
   11.46 +      }
   11.47 +    }.named("cartouche_depth")
   11.48 +
   11.49 +    def cartouche: Parser[String] =
   11.50 +      cartouche_depth(0) ^? { case (x, d) if d == 0 => x }
   11.51 +
   11.52 +    def cartouche_context(ctxt: Context): Parser[(String, Context)] =
   11.53 +    {
   11.54 +      val depth =
   11.55 +        ctxt match {
   11.56 +          case Finished => 0
   11.57 +          case Cartouche(d) => d
   11.58 +          case _ => -1
   11.59 +        }
   11.60 +      if (depth >= 0)
   11.61 +        cartouche_depth(depth) ^^
   11.62 +          { case (x, 0) => (x, Finished)
   11.63 +            case (x, d) => (x, Cartouche(d)) }
   11.64 +      else failure("")
   11.65 +    }
   11.66 +
   11.67 +    val recover_cartouche: Parser[String] =
   11.68 +      cartouche_depth(0) ^^ (_._1)
   11.69 +
   11.70 +    def cartouche_content(source: String): String =
   11.71 +    {
   11.72 +      def err(): Nothing = error("Malformed text cartouche: " + quote(source))
   11.73 +      val source1 =
   11.74 +        Library.try_unprefix(Symbol.open_decoded, source) orElse
   11.75 +          Library.try_unprefix(Symbol.open, source) getOrElse err()
   11.76 +      Library.try_unsuffix(Symbol.close_decoded, source1) orElse
   11.77 +        Library.try_unsuffix(Symbol.close, source1) getOrElse err()
   11.78 +    }
   11.79 +
   11.80 +
   11.81      /* nested comments */
   11.82  
   11.83      private def comment_depth(depth: Int): Parser[(String, Int)] = new Parser[(String, Int)]
   11.84 @@ -309,11 +376,6 @@
   11.85      def comment: Parser[String] =
   11.86        comment_depth(0) ^? { case (x, d) if d == 0 => x }
   11.87  
   11.88 -    def comment_content(source: String): String =
   11.89 -    {
   11.90 -      require(parseAll(comment, source).successful)
   11.91 -      source.substring(2, source.length - 2)
   11.92 -    }
   11.93      def comment_context(ctxt: Context): Parser[(String, Context)] =
   11.94      {
   11.95        val depth =
   11.96 @@ -332,6 +394,12 @@
   11.97      val recover_comment: Parser[String] =
   11.98        comment_depth(0) ^^ (_._1)
   11.99  
  11.100 +    def comment_content(source: String): String =
  11.101 +    {
  11.102 +      require(parseAll(comment, source).successful)
  11.103 +      source.substring(2, source.length - 2)
  11.104 +    }
  11.105 +
  11.106  
  11.107      /* outer syntax tokens */
  11.108  
  11.109 @@ -340,9 +408,10 @@
  11.110        val string = quoted("\"") ^^ (x => Token(Token.Kind.STRING, x))
  11.111        val alt_string = quoted("`") ^^ (x => Token(Token.Kind.ALT_STRING, x))
  11.112        val verb = verbatim ^^ (x => Token(Token.Kind.VERBATIM, x))
  11.113 +      val cart = cartouche ^^ (x => Token(Token.Kind.CARTOUCHE, x))
  11.114        val cmt = comment ^^ (x => Token(Token.Kind.COMMENT, x))
  11.115  
  11.116 -      string | (alt_string | (verb | cmt))
  11.117 +      string | (alt_string | (verb | (cart | cmt)))
  11.118      }
  11.119  
  11.120      private def other_token(is_command: String => Boolean)
  11.121 @@ -380,8 +449,10 @@
  11.122        val space = many1(Symbol.is_blank) ^^ (x => Token(Token.Kind.SPACE, x))
  11.123  
  11.124        val recover_delimited =
  11.125 -        (recover_quoted("\"") | (recover_quoted("`") | (recover_verbatim | recover_comment))) ^^
  11.126 -          (x => Token(Token.Kind.ERROR, x))
  11.127 +        (recover_quoted("\"") |
  11.128 +          (recover_quoted("`") |
  11.129 +            (recover_verbatim |
  11.130 +              (recover_cartouche | recover_comment)))) ^^ (x => Token(Token.Kind.ERROR, x))
  11.131  
  11.132        val bad = one(_ => true) ^^ (x => Token(Token.Kind.ERROR, x))
  11.133  
  11.134 @@ -400,10 +471,11 @@
  11.135        val alt_string =
  11.136          quoted_context("`", ctxt) ^^ { case (x, c) => (Token(Token.Kind.ALT_STRING, x), c) }
  11.137        val verb = verbatim_context(ctxt) ^^ { case (x, c) => (Token(Token.Kind.VERBATIM, x), c) }
  11.138 +      val cart = cartouche_context(ctxt) ^^ { case (x, c) => (Token(Token.Kind.CARTOUCHE, x), c) }
  11.139        val cmt = comment_context(ctxt) ^^ { case (x, c) => (Token(Token.Kind.COMMENT, x), c) }
  11.140        val other = other_token(is_command) ^^ { case x => (x, Finished) }
  11.141  
  11.142 -      string | (alt_string | (verb | (cmt | other)))
  11.143 +      string | (alt_string | (verb | (cart | (cmt | other))))
  11.144      }
  11.145    }
  11.146  }
    12.1 --- a/src/Pure/General/symbol.ML	Fri Jan 17 20:51:36 2014 +0100
    12.2 +++ b/src/Pure/General/symbol.ML	Sat Jan 18 19:15:12 2014 +0100
    12.3 @@ -13,6 +13,7 @@
    12.4    val is_char: symbol -> bool
    12.5    val is_utf8: symbol -> bool
    12.6    val is_symbolic: symbol -> bool
    12.7 +  val is_symbolic_char: symbol -> bool
    12.8    val is_printable: symbol -> bool
    12.9    val eof: symbol
   12.10    val is_eof: symbol -> bool
   12.11 @@ -98,12 +99,17 @@
   12.12  
   12.13  fun is_utf8 s = size s > 0 andalso forall_string (fn c => ord c >= 128) s;
   12.14  
   12.15 +fun raw_symbolic s =
   12.16 +  String.isPrefix "\\<" s andalso String.isSuffix ">" s andalso not (String.isPrefix "\\<^" s);
   12.17 +
   12.18  fun is_symbolic s =
   12.19 -  String.isPrefix "\\<" s andalso String.isSuffix ">" s andalso not (String.isPrefix "\\<^" s);
   12.20 +  s <> "\\<open>" andalso s <> "\\<close>" andalso raw_symbolic s;
   12.21 +
   12.22 +val is_symbolic_char = member (op =) (raw_explode "!#$%&*+-/<=>?@^_|~");
   12.23  
   12.24  fun is_printable s =
   12.25    if is_char s then ord space <= ord s andalso ord s <= ord "~"
   12.26 -  else is_utf8 s orelse is_symbolic s;
   12.27 +  else is_utf8 s orelse raw_symbolic s;
   12.28  
   12.29  
   12.30  (* input source control *)
   12.31 @@ -517,7 +523,7 @@
   12.32  
   12.33  fun symbolic_end (_ :: "\\<^sub>" :: _) = true
   12.34    | symbolic_end ("'" :: ss) = symbolic_end ss
   12.35 -  | symbolic_end (s :: _) = is_symbolic s
   12.36 +  | symbolic_end (s :: _) = raw_symbolic s
   12.37    | symbolic_end [] = false;
   12.38  
   12.39  fun bump_init str =
    13.1 --- a/src/Pure/General/symbol.scala	Fri Jan 17 20:51:36 2014 +0100
    13.2 +++ b/src/Pure/General/symbol.scala	Sat Jan 18 19:15:12 2014 +0100
    13.3 @@ -366,6 +366,12 @@
    13.4      val symbolic = recode_set((for { (sym, _) <- symbols; if raw_symbolic(sym) } yield sym): _*)
    13.5  
    13.6  
    13.7 +    /* cartouches */
    13.8 +
    13.9 +    val open_decoded = decode(open)
   13.10 +    val close_decoded = decode(close)
   13.11 +
   13.12 +
   13.13      /* control symbols */
   13.14  
   13.15      val ctrl_decoded: Set[Symbol] =
   13.16 @@ -420,12 +426,29 @@
   13.17    def is_letdig(sym: Symbol): Boolean = is_letter(sym) || is_digit(sym) || is_quasi(sym)
   13.18    def is_blank(sym: Symbol): Boolean = symbols.blanks.contains(sym)
   13.19  
   13.20 -  def is_symbolic_char(sym: Symbol): Boolean = symbols.sym_chars.contains(sym)
   13.21 -  def is_symbolic(sym: Symbol): Boolean = raw_symbolic(sym) || symbols.symbolic.contains(sym)
   13.22 +
   13.23 +  /* cartouches */
   13.24 +
   13.25 +  val open = "\\<open>"
   13.26 +  val close = "\\<close>"
   13.27 +
   13.28 +  def open_decoded: Symbol = symbols.open_decoded
   13.29 +  def close_decoded: Symbol = symbols.close_decoded
   13.30 +
   13.31 +  def is_open(sym: Symbol): Boolean = sym == open_decoded || sym == open
   13.32 +  def is_close(sym: Symbol): Boolean = sym == close_decoded || sym == close
   13.33 +
   13.34 +
   13.35 +  /* symbols for symbolic identifiers */
   13.36  
   13.37    private def raw_symbolic(sym: Symbol): Boolean =
   13.38      sym.startsWith("\\<") && sym.endsWith(">") && !sym.startsWith("\\<^")
   13.39  
   13.40 +  def is_symbolic(sym: Symbol): Boolean =
   13.41 +    !is_open(sym) && !is_close(sym) && (raw_symbolic(sym) || symbols.symbolic.contains(sym))
   13.42 +
   13.43 +  def is_symbolic_char(sym: Symbol): Boolean = symbols.sym_chars.contains(sym)
   13.44 +
   13.45  
   13.46    /* control symbols */
   13.47  
   13.48 @@ -433,7 +456,7 @@
   13.49      sym.startsWith("\\<^") || symbols.ctrl_decoded.contains(sym)
   13.50  
   13.51    def is_controllable(sym: Symbol): Boolean =
   13.52 -    !is_blank(sym) && !is_ctrl(sym) && !is_malformed(sym)
   13.53 +    !is_blank(sym) && !is_ctrl(sym) && !is_open(sym) && !is_close(sym) && !is_malformed(sym)
   13.54  
   13.55    def sub_decoded: Symbol = symbols.sub_decoded
   13.56    def sup_decoded: Symbol = symbols.sup_decoded
    14.1 --- a/src/Pure/General/symbol_pos.ML	Fri Jan 17 20:51:36 2014 +0100
    14.2 +++ b/src/Pure/General/symbol_pos.ML	Sat Jan 18 19:15:12 2014 +0100
    14.3 @@ -13,6 +13,7 @@
    14.4    val $$$ : Symbol.symbol -> T list -> T list * T list
    14.5    val ~$$$ : Symbol.symbol -> T list -> T list * T list
    14.6    val content: T list -> string
    14.7 +  val range: T list -> Position.range
    14.8    val is_eof: T -> bool
    14.9    val stopper: T Scan.stopper
   14.10    val !!! : Scan.message -> (T list -> 'a) -> T list -> 'a
   14.11 @@ -27,6 +28,12 @@
   14.12    val quote_string_q: string -> string
   14.13    val quote_string_qq: string -> string
   14.14    val quote_string_bq: string -> string
   14.15 +  val scan_cartouche: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
   14.16 +    T list -> T list * T list
   14.17 +  val scan_cartouche_body: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
   14.18 +    T list -> T list * T list
   14.19 +  val recover_cartouche: T list -> T list * T list
   14.20 +  val cartouche_content: T list -> T list
   14.21    val scan_comment: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
   14.22      T list -> T list * T list
   14.23    val scan_comment_body: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
   14.24 @@ -36,7 +43,6 @@
   14.25      (T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source
   14.26    type text = string
   14.27    val implode: T list -> text
   14.28 -  val range: T list -> Position.range
   14.29    val implode_range: Position.T -> Position.T -> T list -> text * Position.range
   14.30    val explode: text * Position.T -> T list
   14.31    val scan_ident: T list -> T list * T list
   14.32 @@ -54,6 +60,11 @@
   14.33  
   14.34  val content = implode o map symbol;
   14.35  
   14.36 +fun range (syms as (_, pos) :: _) =
   14.37 +      let val pos' = List.last syms |-> Position.advance
   14.38 +      in Position.range pos pos' end
   14.39 +  | range [] = Position.no_range;
   14.40 +
   14.41  
   14.42  (* stopper *)
   14.43  
   14.44 @@ -81,6 +92,7 @@
   14.45  
   14.46  fun change_prompt scan = Scan.prompt "# " scan;
   14.47  
   14.48 +fun $$ s = Scan.one (fn x => symbol x = s);
   14.49  fun $$$ s = Scan.one (fn x => symbol x = s) >> single;
   14.50  fun ~$$$ s = Scan.one (fn x => symbol x <> s) >> single;
   14.51  
   14.52 @@ -147,6 +159,47 @@
   14.53  end;
   14.54  
   14.55  
   14.56 +(* nested text cartouches *)
   14.57 +
   14.58 +local
   14.59 +
   14.60 +val scan_cart =
   14.61 +  Scan.depend (fn (d: int) => $$ "\\<open>" >> pair (d + 1)) ||
   14.62 +  Scan.depend (fn 0 => Scan.fail | d => $$ "\\<close>" >> pair (d - 1)) ||
   14.63 +  Scan.lift (Scan.one (fn (s, _) => s <> "\\<close>" andalso Symbol.is_regular s));
   14.64 +
   14.65 +val scan_carts = Scan.pass 0 (Scan.repeat scan_cart);
   14.66 +
   14.67 +val scan_body = change_prompt scan_carts;
   14.68 +
   14.69 +in
   14.70 +
   14.71 +fun scan_cartouche cut =
   14.72 +  $$ "\\<open>" ::: cut "unclosed text cartouche" (scan_body @@@ $$$ "\\<close>");
   14.73 +
   14.74 +fun scan_cartouche_body cut =
   14.75 +  $$ "\\<open>" |-- cut "unclosed text cartouche" (scan_body --| $$ "\\<close>");
   14.76 +
   14.77 +val recover_cartouche =
   14.78 +  $$$ "\\<open>" @@@ scan_carts;
   14.79 +
   14.80 +end;
   14.81 +
   14.82 +fun cartouche_content syms =
   14.83 +  let
   14.84 +    fun err () =
   14.85 +      error ("Malformed text cartouche: " ^ quote (content syms) ^
   14.86 +        Position.here (Position.set_range (range syms)));
   14.87 +  in
   14.88 +    (case syms of
   14.89 +      ("\\<open>", _) :: rest =>
   14.90 +        (case rev rest of
   14.91 +          ("\\<close>", _) :: rrest => rev rrest
   14.92 +        | _ => err ())
   14.93 +    | _ => err ())
   14.94 +  end;
   14.95 +
   14.96 +
   14.97  (* ML-style comments *)
   14.98  
   14.99  local
  14.100 @@ -196,11 +249,6 @@
  14.101  
  14.102  val implode = implode o pad;
  14.103  
  14.104 -fun range (syms as (_, pos) :: _) =
  14.105 -      let val pos' = List.last syms |-> Position.advance
  14.106 -      in Position.range pos pos' end
  14.107 -  | range [] = Position.no_range;
  14.108 -
  14.109  fun implode_range pos1 pos2 syms =
  14.110    let val syms' = (("", pos1) :: syms @ [("", pos2)])
  14.111    in (implode syms', range syms') end;
    15.1 --- a/src/Pure/Isar/args.ML	Fri Jan 17 20:51:36 2014 +0100
    15.2 +++ b/src/Pure/Isar/args.ML	Sat Jan 18 19:15:12 2014 +0100
    15.3 @@ -227,7 +227,7 @@
    15.4  
    15.5  val argument_kinds =
    15.6   [Token.Ident, Token.LongIdent, Token.SymIdent, Token.Var, Token.TypeIdent, Token.TypeVar,
    15.7 -  Token.Nat, Token.Float, Token.String, Token.AltString, Token.Verbatim];
    15.8 +  Token.Nat, Token.Float, Token.String, Token.AltString, Token.Cartouche, Token.Verbatim];
    15.9  
   15.10  fun parse_args is_symid =
   15.11    let
    16.1 --- a/src/Pure/Isar/parse.ML	Fri Jan 17 20:51:36 2014 +0100
    16.2 +++ b/src/Pure/Isar/parse.ML	Sat Jan 18 19:15:12 2014 +0100
    16.3 @@ -32,6 +32,7 @@
    16.4    val string: string parser
    16.5    val alt_string: string parser
    16.6    val verbatim: string parser
    16.7 +  val cartouche: string parser
    16.8    val sync: string parser
    16.9    val eof: string parser
   16.10    val command_name: string -> string parser
   16.11 @@ -185,6 +186,7 @@
   16.12  val string = kind Token.String;
   16.13  val alt_string = kind Token.AltString;
   16.14  val verbatim = kind Token.Verbatim;
   16.15 +val cartouche = kind Token.Cartouche;
   16.16  val sync = kind Token.Sync;
   16.17  val eof = kind Token.EOF;
   16.18  
    17.1 --- a/src/Pure/Isar/token.ML	Fri Jan 17 20:51:36 2014 +0100
    17.2 +++ b/src/Pure/Isar/token.ML	Sat Jan 18 19:15:12 2014 +0100
    17.3 @@ -8,7 +8,7 @@
    17.4  sig
    17.5    datatype kind =
    17.6      Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
    17.7 -    Nat | Float | String | AltString | Verbatim | Space | Comment | InternalValue |
    17.8 +    Nat | Float | String | AltString | Verbatim | Cartouche | Space | Comment | InternalValue |
    17.9      Error of string | Sync | EOF
   17.10    type file = {src_path: Path.T, text: string, pos: Position.T}
   17.11    datatype value =
   17.12 @@ -100,7 +100,7 @@
   17.13  
   17.14  datatype kind =
   17.15    Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
   17.16 -  Nat | Float | String | AltString | Verbatim | Space | Comment | InternalValue |
   17.17 +  Nat | Float | String | AltString | Verbatim | Cartouche | Space | Comment | InternalValue |
   17.18    Error of string | Sync | EOF;
   17.19  
   17.20  datatype T = Token of (Symbol_Pos.text * Position.range) * (kind * string) * slot;
   17.21 @@ -119,6 +119,7 @@
   17.22    | String => "string"
   17.23    | AltString => "back-quoted string"
   17.24    | Verbatim => "verbatim text"
   17.25 +  | Cartouche => "cartouche"
   17.26    | Space => "white space"
   17.27    | Comment => "comment text"
   17.28    | InternalValue => "internal value"
   17.29 @@ -221,6 +222,7 @@
   17.30      String => Symbol_Pos.quote_string_qq x
   17.31    | AltString => Symbol_Pos.quote_string_bq x
   17.32    | Verbatim => enclose "{*" "*}" x
   17.33 +  | Cartouche => cartouche x
   17.34    | Comment => enclose "(*" "*)" x
   17.35    | Sync => ""
   17.36    | EOF => ""
   17.37 @@ -300,16 +302,14 @@
   17.38  
   17.39  (* scan symbolic idents *)
   17.40  
   17.41 -val is_sym_char = member (op =) (raw_explode "!#$%&*+-/<=>?@^_|~");
   17.42 -
   17.43  val scan_symid =
   17.44 -  Scan.many1 (is_sym_char o Symbol_Pos.symbol) ||
   17.45 +  Scan.many1 (Symbol.is_symbolic_char o Symbol_Pos.symbol) ||
   17.46    Scan.one (Symbol.is_symbolic o Symbol_Pos.symbol) >> single;
   17.47  
   17.48  fun is_symid str =
   17.49    (case try Symbol.explode str of
   17.50 -    SOME [s] => Symbol.is_symbolic s orelse is_sym_char s
   17.51 -  | SOME ss => forall is_sym_char ss
   17.52 +    SOME [s] => Symbol.is_symbolic s orelse Symbol.is_symbolic_char s
   17.53 +  | SOME ss => forall Symbol.is_symbolic_char ss
   17.54    | _ => false);
   17.55  
   17.56  fun ident_or_symbolic "begin" = false
   17.57 @@ -333,6 +333,12 @@
   17.58    $$$ "{" @@@ $$$ "*" @@@ (Scan.repeat scan_verb >> flat);
   17.59  
   17.60  
   17.61 +(* scan cartouche *)
   17.62 +
   17.63 +val scan_cartouche =
   17.64 +  Symbol_Pos.scan_pos -- (Symbol_Pos.scan_cartouche_body !!! -- Symbol_Pos.scan_pos);
   17.65 +
   17.66 +
   17.67  (* scan space *)
   17.68  
   17.69  fun space_symbol (s, _) = Symbol.is_blank s andalso s <> "\n";
   17.70 @@ -367,6 +373,7 @@
   17.71    (Symbol_Pos.scan_string_qq err_prefix >> token_range String ||
   17.72      Symbol_Pos.scan_string_bq err_prefix >> token_range AltString ||
   17.73      scan_verbatim >> token_range Verbatim ||
   17.74 +    scan_cartouche >> token_range Cartouche ||
   17.75      scan_comment >> token_range Comment ||
   17.76      scan_space >> token Space ||
   17.77      Scan.one (Symbol.is_sync o Symbol_Pos.symbol) >> (token Sync o single) ||
   17.78 @@ -387,6 +394,7 @@
   17.79    (Symbol_Pos.recover_string_qq ||
   17.80      Symbol_Pos.recover_string_bq ||
   17.81      recover_verbatim ||
   17.82 +    Symbol_Pos.recover_cartouche ||
   17.83      Symbol_Pos.recover_comment ||
   17.84      Scan.one (Symbol.is_regular o Symbol_Pos.symbol) >> single)
   17.85    >> (single o token (Error msg));
    18.1 --- a/src/Pure/Isar/token.scala	Fri Jan 17 20:51:36 2014 +0100
    18.2 +++ b/src/Pure/Isar/token.scala	Sat Jan 18 19:15:12 2014 +0100
    18.3 @@ -26,6 +26,7 @@
    18.4      val STRING = Value("string")
    18.5      val ALT_STRING = Value("back-quoted string")
    18.6      val VERBATIM = Value("verbatim text")
    18.7 +    val CARTOUCHE = Value("cartouche")
    18.8      val SPACE = Value("white space")
    18.9      val COMMENT = Value("comment text")
   18.10      val ERROR = Value("bad input")
   18.11 @@ -74,6 +75,7 @@
   18.12      kind == Token.Kind.STRING ||
   18.13      kind == Token.Kind.ALT_STRING ||
   18.14      kind == Token.Kind.VERBATIM ||
   18.15 +    kind == Token.Kind.CARTOUCHE ||
   18.16      kind == Token.Kind.COMMENT
   18.17    def is_ident: Boolean = kind == Token.Kind.IDENT
   18.18    def is_sym_ident: Boolean = kind == Token.Kind.SYM_IDENT
   18.19 @@ -107,6 +109,7 @@
   18.20      if (kind == Token.Kind.STRING) Scan.Lexicon.empty.quoted_content("\"", source)
   18.21      else if (kind == Token.Kind.ALT_STRING) Scan.Lexicon.empty.quoted_content("`", source)
   18.22      else if (kind == Token.Kind.VERBATIM) Scan.Lexicon.empty.verbatim_content(source)
   18.23 +    else if (kind == Token.Kind.CARTOUCHE) Scan.Lexicon.empty.cartouche_content(source)
   18.24      else if (kind == Token.Kind.COMMENT) Scan.Lexicon.empty.comment_content(source)
   18.25      else source
   18.26  
    19.1 --- a/src/Pure/PIDE/markup.ML	Fri Jan 17 20:51:36 2014 +0100
    19.2 +++ b/src/Pure/PIDE/markup.ML	Sat Jan 18 19:15:12 2014 +0100
    19.3 @@ -59,6 +59,7 @@
    19.4    val literalN: string val literal: T
    19.5    val delimiterN: string val delimiter: T
    19.6    val inner_stringN: string val inner_string: T
    19.7 +  val inner_cartoucheN: string val inner_cartouche: T
    19.8    val inner_commentN: string val inner_comment: T
    19.9    val token_rangeN: string val token_range: T
   19.10    val sortN: string val sort: T
   19.11 @@ -92,6 +93,7 @@
   19.12    val stringN: string val string: T
   19.13    val altstringN: string val altstring: T
   19.14    val verbatimN: string val verbatim: T
   19.15 +  val cartoucheN: string val cartouche: T
   19.16    val commentN: string val comment: T
   19.17    val controlN: string val control: T
   19.18    val tokenN: string val token: Properties.T -> T
   19.19 @@ -307,6 +309,7 @@
   19.20  val (literalN, literal) = markup_elem "literal";
   19.21  val (delimiterN, delimiter) = markup_elem "delimiter";
   19.22  val (inner_stringN, inner_string) = markup_elem "inner_string";
   19.23 +val (inner_cartoucheN, inner_cartouche) = markup_elem "inner_cartouche";
   19.24  val (inner_commentN, inner_comment) = markup_elem "inner_comment";
   19.25  
   19.26  val (token_rangeN, token_range) = markup_elem "token_range";
   19.27 @@ -361,6 +364,7 @@
   19.28  val (stringN, string) = markup_elem "string";
   19.29  val (altstringN, altstring) = markup_elem "altstring";
   19.30  val (verbatimN, verbatim) = markup_elem "verbatim";
   19.31 +val (cartoucheN, cartouche) = markup_elem "cartouche";
   19.32  val (commentN, comment) = markup_elem "comment";
   19.33  val (controlN, control) = markup_elem "control";
   19.34  
    20.1 --- a/src/Pure/PIDE/markup.scala	Fri Jan 17 20:51:36 2014 +0100
    20.2 +++ b/src/Pure/PIDE/markup.scala	Sat Jan 18 19:15:12 2014 +0100
    20.3 @@ -133,6 +133,7 @@
    20.4    val LITERAL = "literal"
    20.5    val DELIMITER = "delimiter"
    20.6    val INNER_STRING = "inner_string"
    20.7 +  val INNER_CARTOUCHE = "inner_cartouche"
    20.8    val INNER_COMMENT = "inner_comment"
    20.9  
   20.10    val TOKEN_RANGE = "token_range"
   20.11 @@ -190,6 +191,7 @@
   20.12    val STRING = "string"
   20.13    val ALTSTRING = "altstring"
   20.14    val VERBATIM = "verbatim"
   20.15 +  val CARTOUCHE = "cartouche"
   20.16    val COMMENT = "comment"
   20.17    val CONTROL = "control"
   20.18  
    21.1 --- a/src/Pure/Syntax/lexicon.ML	Fri Jan 17 20:51:36 2014 +0100
    21.2 +++ b/src/Pure/Syntax/lexicon.ML	Sat Jan 18 19:15:12 2014 +0100
    21.3 @@ -25,7 +25,7 @@
    21.4    val is_tid: string -> bool
    21.5    datatype token_kind =
    21.6      Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy |
    21.7 -    NumSy | FloatSy | XNumSy | StrSy | Space | Comment | EOF
    21.8 +    NumSy | FloatSy | XNumSy | StrSy | Cartouche | Space | Comment | EOF
    21.9    datatype token = Token of token_kind * string * Position.range
   21.10    val str_of_token: token -> string
   21.11    val pos_of_token: token -> Position.T
   21.12 @@ -120,7 +120,7 @@
   21.13  
   21.14  datatype token_kind =
   21.15    Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy |
   21.16 -  NumSy | FloatSy | XNumSy | StrSy | Space | Comment | EOF;
   21.17 +  NumSy | FloatSy | XNumSy | StrSy | Cartouche | Space | Comment | EOF;
   21.18  
   21.19  datatype token = Token of token_kind * string * Position.range;
   21.20  
   21.21 @@ -160,7 +160,8 @@
   21.22    ("num_token", NumSy),
   21.23    ("float_token", FloatSy),
   21.24    ("xnum_token", XNumSy),
   21.25 -  ("str_token", StrSy)];
   21.26 +  ("str_token", StrSy),
   21.27 +  ("cartouche", Cartouche)];
   21.28  
   21.29  val terminals = map #1 terminal_kinds;
   21.30  val is_terminal = member (op =) terminals;
   21.31 @@ -175,13 +176,14 @@
   21.32  
   21.33  val token_kind_markup =
   21.34   fn TFreeSy => Markup.tfree
   21.35 -  | TVarSy  => Markup.tvar
   21.36 -  | NumSy   => Markup.numeral
   21.37 +  | TVarSy => Markup.tvar
   21.38 +  | NumSy => Markup.numeral
   21.39    | FloatSy => Markup.numeral
   21.40 -  | XNumSy  => Markup.numeral
   21.41 -  | StrSy   => Markup.inner_string
   21.42 +  | XNumSy => Markup.numeral
   21.43 +  | StrSy => Markup.inner_string
   21.44 +  | Cartouche => Markup.inner_cartouche
   21.45    | Comment => Markup.inner_comment
   21.46 -  | _       => Markup.empty;
   21.47 +  | _ => Markup.empty;
   21.48  
   21.49  fun report_of_token (Token (kind, s, (pos, _))) =
   21.50    let val markup = if kind = Literal then literal_markup s else token_kind_markup kind
   21.51 @@ -267,6 +269,7 @@
   21.52      val scan_lit = Scan.literal lex >> token Literal;
   21.53  
   21.54      val scan_token =
   21.55 +      Symbol_Pos.scan_cartouche !!! >> token Cartouche ||
   21.56        Symbol_Pos.scan_comment !!! >> token Comment ||
   21.57        Scan.max token_leq scan_lit scan_val ||
   21.58        scan_str >> token StrSy ||
    22.1 --- a/src/Pure/Thy/html.ML	Fri Jan 17 20:51:36 2014 +0100
    22.2 +++ b/src/Pure/Thy/html.ML	Sat Jan 18 19:15:12 2014 +0100
    22.3 @@ -188,6 +188,8 @@
    22.4      ("\\<longleftrightarrow>", (3, "&lt;-&gt;")),
    22.5      ("\\<longrightarrow>", (3, "--&gt;")),
    22.6      ("\\<rightarrow>", (2, "-&gt;")),
    22.7 +    ("\\<open>", (1, "&#8249;")),
    22.8 +    ("\\<close>", (1, "&#8250;")),
    22.9      ("\\<^bsub>", (0, hidden "&#8664;" ^ "<sub>")),
   22.10      ("\\<^esub>", (0, hidden "&#8665;" ^ "</sub>")),
   22.11      ("\\<^bsup>", (0, hidden "&#8663;" ^ "<sup>")),
    23.1 --- a/src/Pure/Thy/latex.ML	Fri Jan 17 20:51:36 2014 +0100
    23.2 +++ b/src/Pure/Thy/latex.ML	Sat Jan 18 19:15:12 2014 +0100
    23.3 @@ -125,6 +125,8 @@
    23.4          val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
    23.5          val out = implode (map output_syms_antiq ants);
    23.6        in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
    23.7 +    else if Token.is_kind Token.Cartouche tok then
    23.8 +      enclose "{\\isacartoucheopen}" "{\\isacartoucheclose}" (output_syms s)
    23.9      else output_syms s
   23.10    end;
   23.11  
    24.1 --- a/src/Pure/Thy/thy_syntax.ML	Fri Jan 17 20:51:36 2014 +0100
    24.2 +++ b/src/Pure/Thy/thy_syntax.ML	Sat Jan 18 19:15:12 2014 +0100
    24.3 @@ -56,6 +56,7 @@
    24.4    | Token.String        => (Markup.string, "")
    24.5    | Token.AltString     => (Markup.altstring, "")
    24.6    | Token.Verbatim      => (Markup.verbatim, "")
    24.7 +  | Token.Cartouche     => (Markup.cartouche, "")
    24.8    | Token.Space         => (Markup.empty, "")
    24.9    | Token.Comment       => (Markup.comment, "")
   24.10    | Token.InternalValue => (Markup.empty, "")
    25.1 --- a/src/Pure/library.ML	Fri Jan 17 20:51:36 2014 +0100
    25.2 +++ b/src/Pure/library.ML	Sat Jan 18 19:15:12 2014 +0100
    25.3 @@ -139,6 +139,7 @@
    25.4    val enclose: string -> string -> string -> string
    25.5    val unenclose: string -> string
    25.6    val quote: string -> string
    25.7 +  val cartouche: string -> string
    25.8    val space_implode: string -> string list -> string
    25.9    val commas: string list -> string
   25.10    val commas_quote: string list -> string
   25.11 @@ -729,6 +730,8 @@
   25.12  (*simple quoting (does not escape special chars)*)
   25.13  val quote = enclose "\"" "\"";
   25.14  
   25.15 +val cartouche = enclose "\\<open>" "\\<close>";
   25.16 +
   25.17  fun space_implode a bs = implode (separate a bs);
   25.18  
   25.19  val commas = space_implode ", ";
    26.1 --- a/src/Pure/library.scala	Fri Jan 17 20:51:36 2014 +0100
    26.2 +++ b/src/Pure/library.scala	Sat Jan 18 19:15:12 2014 +0100
    26.3 @@ -110,6 +110,9 @@
    26.4    def try_unprefix(prfx: String, s: String): Option[String] =
    26.5      if (s.startsWith(prfx)) Some(s.substring(prfx.length)) else None
    26.6  
    26.7 +  def try_unsuffix(sffx: String, s: String): Option[String] =
    26.8 +    if (s.endsWith(sffx)) Some(s.substring(0, s.length - sffx.length)) else None
    26.9 +
   26.10    def trim_line(s: String): String =
   26.11      if (s.endsWith("\r\n")) s.substring(0, s.length - 2)
   26.12      else if (s.endsWith("\r") || s.endsWith("\n")) s.substring(0, s.length - 1)
    27.1 --- a/src/Pure/pure_thy.ML	Fri Jan 17 20:51:36 2014 +0100
    27.2 +++ b/src/Pure/pure_thy.ML	Sat Jan 18 19:15:12 2014 +0100
    27.3 @@ -71,7 +71,7 @@
    27.4          "any", "prop'", "num_const", "float_const", "xnum_const", "num_position",
    27.5          "float_position", "xnum_position", "index", "struct", "tid_position",
    27.6          "tvar_position", "id_position", "longid_position", "var_position", "str_position",
    27.7 -        "type_name", "class_name"]))
    27.8 +        "cartouche_position", "type_name", "class_name"]))
    27.9    #> Sign.add_syntax_i (map (fn x => (x, typ "'a", NoSyn)) token_markers)
   27.10    #> Sign.add_syntax_i
   27.11     [("",            typ "prop' => prop",               Delimfix "_"),
   27.12 @@ -155,6 +155,7 @@
   27.13      ("_position",   typ "longid => longid_position",   Delimfix "_"),
   27.14      ("_position",   typ "var => var_position",         Delimfix "_"),
   27.15      ("_position",   typ "str_token => str_position",   Delimfix "_"),
   27.16 +    ("_position",   typ "cartouche => cartouche_position", Delimfix "_"),
   27.17      ("_type_constraint_", typ "'a",                    NoSyn),
   27.18      ("_context_const", typ "id_position => logic",     Delimfix "CONST _"),
   27.19      ("_context_const", typ "id_position => aprop",     Delimfix "CONST _"),
    28.1 --- a/src/Tools/jEdit/etc/options	Fri Jan 17 20:51:36 2014 +0100
    28.2 +++ b/src/Tools/jEdit/etc/options	Sat Jan 18 19:15:12 2014 +0100
    28.3 @@ -92,6 +92,7 @@
    28.4  option var_color : string = "00009BFF"
    28.5  option inner_numeral_color : string = "FF0000FF"
    28.6  option inner_quoted_color : string = "D2691EFF"
    28.7 +option inner_cartouche_color : string = "CC6600FF"
    28.8  option inner_comment_color : string = "8B0000FF"
    28.9  option dynamic_color : string = "7BA428FF"
   28.10  
    29.1 --- a/src/Tools/jEdit/src/rendering.scala	Fri Jan 17 20:51:36 2014 +0100
    29.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sat Jan 18 19:15:12 2014 +0100
    29.3 @@ -99,6 +99,7 @@
    29.4        Token.Kind.STRING -> LITERAL1,
    29.5        Token.Kind.ALT_STRING -> LITERAL2,
    29.6        Token.Kind.VERBATIM -> COMMENT3,
    29.7 +      Token.Kind.CARTOUCHE -> COMMENT4,
    29.8        Token.Kind.SPACE -> NULL,
    29.9        Token.Kind.COMMENT -> COMMENT1,
   29.10        Token.Kind.ERROR -> INVALID
   29.11 @@ -156,6 +157,7 @@
   29.12    val var_color = color_value("var_color")
   29.13    val inner_numeral_color = color_value("inner_numeral_color")
   29.14    val inner_quoted_color = color_value("inner_quoted_color")
   29.15 +  val inner_cartouche_color = color_value("inner_cartouche_color")
   29.16    val inner_comment_color = color_value("inner_comment_color")
   29.17    val dynamic_color = color_value("dynamic_color")
   29.18  
   29.19 @@ -593,6 +595,7 @@
   29.20        Markup.BOUND -> bound_color,
   29.21        Markup.VAR -> var_color,
   29.22        Markup.INNER_STRING -> inner_quoted_color,
   29.23 +      Markup.INNER_CARTOUCHE -> inner_cartouche_color,
   29.24        Markup.INNER_COMMENT -> inner_comment_color,
   29.25        Markup.DYNAMIC_FACT -> dynamic_color,
   29.26        Markup.ML_KEYWORD -> keyword1_color,