# HG changeset patch # User wenzelm # Date 1390068912 -3600 # Node ID 8e82439758602bfcfab9624950005ea2e547c08d # Parent b493662154173cd4713f35f7c1113052aa308c32 support for nested text cartouches; clarified Symbol.is_symbolic: exclude \ and \; diff -r b49366215417 -r 8e8243975860 etc/isabelle.css --- a/etc/isabelle.css Fri Jan 17 20:51:36 2014 +0100 +++ b/etc/isabelle.css Sat Jan 18 19:15:12 2014 +0100 @@ -30,6 +30,7 @@ .literal { font-weight: bold; } .delimiter { } .inner_string { color: #D2691E; } +.inner_cartouche { color: #CC6600; } .inner_comment { color: #8B0000; } .bold { font-weight: bold; } @@ -40,6 +41,7 @@ .string { color: #008B00; } .altstring { color: #8B8B00; } .verbatim { color: #00008B; } +.cartouche { color: #CC6600; } .comment { color: #8B0000; } .control { background-color: #FF6A6A; } .bad { background-color: #FF6A6A; } diff -r b49366215417 -r 8e8243975860 etc/isar-keywords.el --- a/etc/isar-keywords.el Fri Jan 17 20:51:36 2014 +0100 +++ b/etc/isar-keywords.el Sat Jan 18 19:15:12 2014 +0100 @@ -38,6 +38,7 @@ "bundle" "by" "cannot_undo" + "cartouche" "case" "case_of_simps" "cd" @@ -389,6 +390,7 @@ (defconst isar-keywords-diag '("ML_command" "ML_val" + "cartouche" "class_deps" "code_deps" "code_thms" diff -r b49366215417 -r 8e8243975860 etc/symbols --- a/etc/symbols Fri Jan 17 20:51:36 2014 +0100 +++ b/etc/symbols Sat Jan 18 19:15:12 2014 +0100 @@ -348,6 +348,8 @@ \ code: 0x0002dd \ code: 0x0003f5 \ code: 0x0023ce +\ code: 0x002039 abbrev: << font: IsabelleText +\ code: 0x00203a abbrev: >> font: IsabelleText \<^sub> code: 0x0021e9 group: control font: IsabelleText \<^sup> code: 0x0021e7 group: control font: IsabelleText \<^bold> code: 0x002759 group: control font: IsabelleText diff -r b49366215417 -r 8e8243975860 lib/texinputs/isabelle.sty --- a/lib/texinputs/isabelle.sty Fri Jan 17 20:51:36 2014 +0100 +++ b/lib/texinputs/isabelle.sty Sat Jan 18 19:15:12 2014 +0100 @@ -97,6 +97,8 @@ \chardef\isachartilde=`\~% \def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}% \def\isacharverbatimclose{\isacharasterisk\isacharbraceright}% +\def\isacartoucheopen{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}% +\def\isacartoucheclose{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}% } diff -r b49366215417 -r 8e8243975860 lib/texinputs/isabellesym.sty --- a/lib/texinputs/isabellesym.sty Fri Jan 17 20:51:36 2014 +0100 +++ b/lib/texinputs/isabellesym.sty Sat Jan 18 19:15:12 2014 +0100 @@ -354,3 +354,6 @@ \newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}} \newcommand{\isasymthen}{\isamath{\mathbin{>\!\!\!>}}} \newcommand{\isasymsome}{\isamath{\epsilon\,}} +\newcommand{\isasymopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}} +\newcommand{\isasymclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}} + diff -r b49366215417 -r 8e8243975860 src/Doc/IsarRef/Inner_Syntax.thy --- a/src/Doc/IsarRef/Inner_Syntax.thy Fri Jan 17 20:51:36 2014 +0100 +++ b/src/Doc/IsarRef/Inner_Syntax.thy Sat Jan 18 19:15:12 2014 +0100 @@ -633,14 +633,16 @@ @{syntax_def (inner) xnum_token} & = & @{verbatim "#"}@{syntax_ref nat}@{text " | "}@{verbatim "#-"}@{syntax_ref nat} \\ @{syntax_def (inner) str_token} & = & @{verbatim "''"} @{text "\"} @{verbatim "''"} \\ + @{syntax_def (inner) cartouche} & = & @{verbatim "\"} @{text "\"} @{verbatim "\"} \\ \end{supertabular} \end{center} The token categories @{syntax (inner) num_token}, @{syntax (inner) - float_token}, @{syntax (inner) xnum_token}, and @{syntax (inner) - str_token} are not used in Pure. Object-logics may implement numerals - and string constants by adding appropriate syntax declarations, - together with some translation functions (e.g.\ see Isabelle/HOL). + float_token}, @{syntax (inner) xnum_token}, @{syntax (inner) + str_token}, and @{syntax (inner) cartouche} are not used in Pure. + Object-logics may implement numerals and string literals by adding + appropriate syntax declarations, together with some translation + functions (e.g.\ see Isabelle/HOL). The derived categories @{syntax_def (inner) num_const}, @{syntax_def (inner) float_const}, and @{syntax_def (inner) num_const} provide diff -r b49366215417 -r 8e8243975860 src/Doc/IsarRef/Outer_Syntax.thy --- a/src/Doc/IsarRef/Outer_Syntax.thy Fri Jan 17 20:51:36 2014 +0100 +++ b/src/Doc/IsarRef/Outer_Syntax.thy Sat Jan 18 19:15:12 2014 +0100 @@ -147,6 +147,7 @@ @{syntax_def typevar} & = & @{verbatim "?"}@{text "typefree | "}@{verbatim "?"}@{text typefree}@{verbatim "."}@{text nat} \\ @{syntax_def string} & = & @{verbatim "\""} @{text "\"} @{verbatim "\""} \\ @{syntax_def altstring} & = & @{verbatim "`"} @{text "\"} @{verbatim "`"} \\ + @{syntax_def cartouche} & = & @{verbatim "\"} @{text "\"} @{verbatim "\"} \\ @{syntax_def verbatim} & = & @{verbatim "{*"} @{text "\"} @{verbatim "*"}@{verbatim "}"} \\[1ex] @{text letter} & = & @{text "latin | "}@{verbatim "\\"}@{verbatim "<"}@{text latin}@{verbatim ">"}@{text " | "}@{verbatim "\\"}@{verbatim "<"}@{text "latin latin"}@{verbatim ">"}@{text " | greek |"} \\ @@ -191,6 +192,11 @@ text is {\LaTeX} source, one may usually add some blank or comment to avoid the critical character sequence. + A @{syntax_ref cartouche} consists of arbitrary text, with properly + balanced blocks of ``@{verbatim "\"}~@{text "\"}~@{verbatim + "\"}''. Note that the rendering of cartouche delimiters is + usually like this: ``@{text "\ \ \"}''. + Source comments take the form @{verbatim "(*"}~@{text "\"}~@{verbatim "*)"} and may be nested, although the user-interface might prevent this. Note that this form indicates source comments diff -r b49366215417 -r 8e8243975860 src/HOL/ROOT --- a/src/HOL/ROOT Fri Jan 17 20:51:36 2014 +0100 +++ b/src/HOL/ROOT Sat Jan 18 19:15:12 2014 +0100 @@ -562,6 +562,7 @@ SVC_Oracle Simps_Case_Conv_Examples ML + Cartouche_Examples theories [skip_proofs = false] Meson_Test theories [condition = SVC_HOME] diff -r b49366215417 -r 8e8243975860 src/HOL/ex/Cartouche_Examples.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Cartouche_Examples.thy Sat Jan 18 19:15:12 2014 +0100 @@ -0,0 +1,61 @@ +header {* Some examples with text cartouches *} + +theory Cartouche_Examples +imports Main +keywords "cartouche" :: diag +begin + +subsection {* Outer syntax *} + +ML {* + Outer_Syntax.improper_command @{command_spec "cartouche"} "" + (Parse.cartouche >> (fn s => + Toplevel.imperative (fn () => writeln s))) +*} + +cartouche \abc\ +cartouche \abc \\\\\ xzy\ + + +subsection {* Inner syntax *} + +syntax "_string_cartouche" :: "cartouche_position \ string" ("STR _") + +parse_translation {* + let + val mk_nib = + Syntax.const o Lexicon.mark_const o + fst o Term.dest_Const o HOLogic.mk_nibble; + + fun mk_char (s, pos) = + let + val c = + if Symbol.is_ascii s then ord s + else if s = "" then 10 + else error ("String literal contains illegal symbol: " ^ quote s ^ Position.here pos); + in Syntax.const @{const_syntax Char} $ mk_nib (c div 16) $ mk_nib (c mod 16) end; + + fun mk_string [] = Const (@{const_syntax Nil}, @{typ string}) + | mk_string (s :: ss) = + Syntax.const @{const_syntax Cons} $ mk_char s $ mk_string ss; + + fun string_tr ctxt args = + let fun err () = raise TERM ("string_tr", []) in + (case args of + [(c as Const (@{syntax_const "_constrain"}, _)) $ Free (s, _) $ p] => + (case Term_Position.decode_position p of + SOME (pos, _) => + c $ mk_string (Symbol_Pos.cartouche_content (Symbol_Pos.explode (s, pos))) $ p + | NONE => err ()) + | _ => err ()) + end; + in + [(@{syntax_const "_string_cartouche"}, string_tr)] + end +*} + +term "STR \\" +term "STR \abc\" +lemma "STR \abc\ @ STR \xyz\ = STR \abcxyz\" by simp + +end diff -r b49366215417 -r 8e8243975860 src/Pure/General/pretty.ML --- a/src/Pure/General/pretty.ML Fri Jan 17 20:51:36 2014 +0100 +++ b/src/Pure/General/pretty.ML Sat Jan 18 19:15:12 2014 +0100 @@ -51,6 +51,7 @@ val block_enclose: T * T -> T list -> T val quote: T -> T val backquote: T -> T + val cartouche: T -> T val separate: string -> T list -> T list val commas: T list -> T list val enclose: string -> string -> T list -> T @@ -182,6 +183,7 @@ fun quote prt = blk (1, [str "\"", prt, str "\""]); fun backquote prt = blk (1, [str "`", prt, str "`"]); +fun cartouche prt = blk (1, [str "\\", prt, str "\\"]); fun separate sep prts = flat (Library.separate [str sep, brk 1] (map single prts)); diff -r b49366215417 -r 8e8243975860 src/Pure/General/scan.scala --- a/src/Pure/General/scan.scala Fri Jan 17 20:51:36 2014 +0100 +++ b/src/Pure/General/scan.scala Sat Jan 18 19:15:12 2014 +0100 @@ -23,6 +23,7 @@ case object Finished extends Context case class Quoted(quote: String) extends Context case object Verbatim extends Context + case class Cartouche(depth: Int) extends Context case class Comment(depth: Int) extends Context @@ -274,6 +275,72 @@ "{*" ~ verbatim_body ^^ { case x ~ y => x + y } + /* nested text cartouches */ + + private def cartouche_depth(depth: Int): Parser[(String, Int)] = new Parser[(String, Int)] + { + require(depth >= 0) + + def apply(in: Input) = + { + val start = in.offset + val end = in.source.length + val matcher = new Symbol.Matcher(in.source) + + var i = start + var d = depth + var finished = false + while (!finished) { + if (i < end) { + val n = matcher(i, end) + val sym = in.source.subSequence(i, i + n).toString + + if (Symbol.is_open(sym)) { i += n; d += 1 } + else if (d > 0) { + i += n + if (Symbol.is_close(sym)) d -= 1 + } + else finished = true + } + else finished = true + } + if (i == start) Failure("bad input", in) + else Success((in.source.subSequence(start, i).toString, d), in.drop(i - start)) + } + }.named("cartouche_depth") + + def cartouche: Parser[String] = + cartouche_depth(0) ^? { case (x, d) if d == 0 => x } + + def cartouche_context(ctxt: Context): Parser[(String, Context)] = + { + val depth = + ctxt match { + case Finished => 0 + case Cartouche(d) => d + case _ => -1 + } + if (depth >= 0) + cartouche_depth(depth) ^^ + { case (x, 0) => (x, Finished) + case (x, d) => (x, Cartouche(d)) } + else failure("") + } + + val recover_cartouche: Parser[String] = + cartouche_depth(0) ^^ (_._1) + + def cartouche_content(source: String): String = + { + def err(): Nothing = error("Malformed text cartouche: " + quote(source)) + val source1 = + Library.try_unprefix(Symbol.open_decoded, source) orElse + Library.try_unprefix(Symbol.open, source) getOrElse err() + Library.try_unsuffix(Symbol.close_decoded, source1) orElse + Library.try_unsuffix(Symbol.close, source1) getOrElse err() + } + + /* nested comments */ private def comment_depth(depth: Int): Parser[(String, Int)] = new Parser[(String, Int)] @@ -309,11 +376,6 @@ def comment: Parser[String] = comment_depth(0) ^? { case (x, d) if d == 0 => x } - def comment_content(source: String): String = - { - require(parseAll(comment, source).successful) - source.substring(2, source.length - 2) - } def comment_context(ctxt: Context): Parser[(String, Context)] = { val depth = @@ -332,6 +394,12 @@ val recover_comment: Parser[String] = comment_depth(0) ^^ (_._1) + def comment_content(source: String): String = + { + require(parseAll(comment, source).successful) + source.substring(2, source.length - 2) + } + /* outer syntax tokens */ @@ -340,9 +408,10 @@ val string = quoted("\"") ^^ (x => Token(Token.Kind.STRING, x)) val alt_string = quoted("`") ^^ (x => Token(Token.Kind.ALT_STRING, x)) val verb = verbatim ^^ (x => Token(Token.Kind.VERBATIM, x)) + val cart = cartouche ^^ (x => Token(Token.Kind.CARTOUCHE, x)) val cmt = comment ^^ (x => Token(Token.Kind.COMMENT, x)) - string | (alt_string | (verb | cmt)) + string | (alt_string | (verb | (cart | cmt))) } private def other_token(is_command: String => Boolean) @@ -380,8 +449,10 @@ val space = many1(Symbol.is_blank) ^^ (x => Token(Token.Kind.SPACE, x)) val recover_delimited = - (recover_quoted("\"") | (recover_quoted("`") | (recover_verbatim | recover_comment))) ^^ - (x => Token(Token.Kind.ERROR, x)) + (recover_quoted("\"") | + (recover_quoted("`") | + (recover_verbatim | + (recover_cartouche | recover_comment)))) ^^ (x => Token(Token.Kind.ERROR, x)) val bad = one(_ => true) ^^ (x => Token(Token.Kind.ERROR, x)) @@ -400,10 +471,11 @@ val alt_string = quoted_context("`", ctxt) ^^ { case (x, c) => (Token(Token.Kind.ALT_STRING, x), c) } val verb = verbatim_context(ctxt) ^^ { case (x, c) => (Token(Token.Kind.VERBATIM, x), c) } + val cart = cartouche_context(ctxt) ^^ { case (x, c) => (Token(Token.Kind.CARTOUCHE, x), c) } val cmt = comment_context(ctxt) ^^ { case (x, c) => (Token(Token.Kind.COMMENT, x), c) } val other = other_token(is_command) ^^ { case x => (x, Finished) } - string | (alt_string | (verb | (cmt | other))) + string | (alt_string | (verb | (cart | (cmt | other)))) } } } diff -r b49366215417 -r 8e8243975860 src/Pure/General/symbol.ML --- a/src/Pure/General/symbol.ML Fri Jan 17 20:51:36 2014 +0100 +++ b/src/Pure/General/symbol.ML Sat Jan 18 19:15:12 2014 +0100 @@ -13,6 +13,7 @@ val is_char: symbol -> bool val is_utf8: symbol -> bool val is_symbolic: symbol -> bool + val is_symbolic_char: symbol -> bool val is_printable: symbol -> bool val eof: symbol val is_eof: symbol -> bool @@ -98,12 +99,17 @@ fun is_utf8 s = size s > 0 andalso forall_string (fn c => ord c >= 128) s; +fun raw_symbolic s = + String.isPrefix "\\<" s andalso String.isSuffix ">" s andalso not (String.isPrefix "\\<^" s); + fun is_symbolic s = - String.isPrefix "\\<" s andalso String.isSuffix ">" s andalso not (String.isPrefix "\\<^" s); + s <> "\\" andalso s <> "\\" andalso raw_symbolic s; + +val is_symbolic_char = member (op =) (raw_explode "!#$%&*+-/<=>?@^_|~"); fun is_printable s = if is_char s then ord space <= ord s andalso ord s <= ord "~" - else is_utf8 s orelse is_symbolic s; + else is_utf8 s orelse raw_symbolic s; (* input source control *) @@ -517,7 +523,7 @@ fun symbolic_end (_ :: "\\<^sub>" :: _) = true | symbolic_end ("'" :: ss) = symbolic_end ss - | symbolic_end (s :: _) = is_symbolic s + | symbolic_end (s :: _) = raw_symbolic s | symbolic_end [] = false; fun bump_init str = diff -r b49366215417 -r 8e8243975860 src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Fri Jan 17 20:51:36 2014 +0100 +++ b/src/Pure/General/symbol.scala Sat Jan 18 19:15:12 2014 +0100 @@ -366,6 +366,12 @@ val symbolic = recode_set((for { (sym, _) <- symbols; if raw_symbolic(sym) } yield sym): _*) + /* cartouches */ + + val open_decoded = decode(open) + val close_decoded = decode(close) + + /* control symbols */ val ctrl_decoded: Set[Symbol] = @@ -420,12 +426,29 @@ def is_letdig(sym: Symbol): Boolean = is_letter(sym) || is_digit(sym) || is_quasi(sym) def is_blank(sym: Symbol): Boolean = symbols.blanks.contains(sym) - def is_symbolic_char(sym: Symbol): Boolean = symbols.sym_chars.contains(sym) - def is_symbolic(sym: Symbol): Boolean = raw_symbolic(sym) || symbols.symbolic.contains(sym) + + /* cartouches */ + + val open = "\\" + val close = "\\" + + def open_decoded: Symbol = symbols.open_decoded + def close_decoded: Symbol = symbols.close_decoded + + def is_open(sym: Symbol): Boolean = sym == open_decoded || sym == open + def is_close(sym: Symbol): Boolean = sym == close_decoded || sym == close + + + /* symbols for symbolic identifiers */ private def raw_symbolic(sym: Symbol): Boolean = sym.startsWith("\\<") && sym.endsWith(">") && !sym.startsWith("\\<^") + def is_symbolic(sym: Symbol): Boolean = + !is_open(sym) && !is_close(sym) && (raw_symbolic(sym) || symbols.symbolic.contains(sym)) + + def is_symbolic_char(sym: Symbol): Boolean = symbols.sym_chars.contains(sym) + /* control symbols */ @@ -433,7 +456,7 @@ sym.startsWith("\\<^") || symbols.ctrl_decoded.contains(sym) def is_controllable(sym: Symbol): Boolean = - !is_blank(sym) && !is_ctrl(sym) && !is_malformed(sym) + !is_blank(sym) && !is_ctrl(sym) && !is_open(sym) && !is_close(sym) && !is_malformed(sym) def sub_decoded: Symbol = symbols.sub_decoded def sup_decoded: Symbol = symbols.sup_decoded diff -r b49366215417 -r 8e8243975860 src/Pure/General/symbol_pos.ML --- a/src/Pure/General/symbol_pos.ML Fri Jan 17 20:51:36 2014 +0100 +++ b/src/Pure/General/symbol_pos.ML Sat Jan 18 19:15:12 2014 +0100 @@ -13,6 +13,7 @@ val $$$ : Symbol.symbol -> T list -> T list * T list val ~$$$ : Symbol.symbol -> T list -> T list * T list val content: T list -> string + val range: T list -> Position.range val is_eof: T -> bool val stopper: T Scan.stopper val !!! : Scan.message -> (T list -> 'a) -> T list -> 'a @@ -27,6 +28,12 @@ val quote_string_q: string -> string val quote_string_qq: string -> string val quote_string_bq: string -> string + val scan_cartouche: (string -> (T list -> T list * T list) -> T list -> T list * T list) -> + T list -> T list * T list + val scan_cartouche_body: (string -> (T list -> T list * T list) -> T list -> T list * T list) -> + T list -> T list * T list + val recover_cartouche: T list -> T list * T list + val cartouche_content: T list -> T list val scan_comment: (string -> (T list -> T list * T list) -> T list -> T list * T list) -> T list -> T list * T list val scan_comment_body: (string -> (T list -> T list * T list) -> T list -> T list * T list) -> @@ -36,7 +43,6 @@ (T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source type text = string val implode: T list -> text - val range: T list -> Position.range val implode_range: Position.T -> Position.T -> T list -> text * Position.range val explode: text * Position.T -> T list val scan_ident: T list -> T list * T list @@ -54,6 +60,11 @@ val content = implode o map symbol; +fun range (syms as (_, pos) :: _) = + let val pos' = List.last syms |-> Position.advance + in Position.range pos pos' end + | range [] = Position.no_range; + (* stopper *) @@ -81,6 +92,7 @@ fun change_prompt scan = Scan.prompt "# " scan; +fun $$ s = Scan.one (fn x => symbol x = s); fun $$$ s = Scan.one (fn x => symbol x = s) >> single; fun ~$$$ s = Scan.one (fn x => symbol x <> s) >> single; @@ -147,6 +159,47 @@ end; +(* nested text cartouches *) + +local + +val scan_cart = + Scan.depend (fn (d: int) => $$ "\\" >> pair (d + 1)) || + Scan.depend (fn 0 => Scan.fail | d => $$ "\\" >> pair (d - 1)) || + Scan.lift (Scan.one (fn (s, _) => s <> "\\" andalso Symbol.is_regular s)); + +val scan_carts = Scan.pass 0 (Scan.repeat scan_cart); + +val scan_body = change_prompt scan_carts; + +in + +fun scan_cartouche cut = + $$ "\\" ::: cut "unclosed text cartouche" (scan_body @@@ $$$ "\\"); + +fun scan_cartouche_body cut = + $$ "\\" |-- cut "unclosed text cartouche" (scan_body --| $$ "\\"); + +val recover_cartouche = + $$$ "\\" @@@ scan_carts; + +end; + +fun cartouche_content syms = + let + fun err () = + error ("Malformed text cartouche: " ^ quote (content syms) ^ + Position.here (Position.set_range (range syms))); + in + (case syms of + ("\\", _) :: rest => + (case rev rest of + ("\\", _) :: rrest => rev rrest + | _ => err ()) + | _ => err ()) + end; + + (* ML-style comments *) local @@ -196,11 +249,6 @@ val implode = implode o pad; -fun range (syms as (_, pos) :: _) = - let val pos' = List.last syms |-> Position.advance - in Position.range pos pos' end - | range [] = Position.no_range; - fun implode_range pos1 pos2 syms = let val syms' = (("", pos1) :: syms @ [("", pos2)]) in (implode syms', range syms') end; diff -r b49366215417 -r 8e8243975860 src/Pure/Isar/args.ML --- a/src/Pure/Isar/args.ML Fri Jan 17 20:51:36 2014 +0100 +++ b/src/Pure/Isar/args.ML Sat Jan 18 19:15:12 2014 +0100 @@ -227,7 +227,7 @@ val argument_kinds = [Token.Ident, Token.LongIdent, Token.SymIdent, Token.Var, Token.TypeIdent, Token.TypeVar, - Token.Nat, Token.Float, Token.String, Token.AltString, Token.Verbatim]; + Token.Nat, Token.Float, Token.String, Token.AltString, Token.Cartouche, Token.Verbatim]; fun parse_args is_symid = let diff -r b49366215417 -r 8e8243975860 src/Pure/Isar/parse.ML --- a/src/Pure/Isar/parse.ML Fri Jan 17 20:51:36 2014 +0100 +++ b/src/Pure/Isar/parse.ML Sat Jan 18 19:15:12 2014 +0100 @@ -32,6 +32,7 @@ val string: string parser val alt_string: string parser val verbatim: string parser + val cartouche: string parser val sync: string parser val eof: string parser val command_name: string -> string parser @@ -185,6 +186,7 @@ val string = kind Token.String; val alt_string = kind Token.AltString; val verbatim = kind Token.Verbatim; +val cartouche = kind Token.Cartouche; val sync = kind Token.Sync; val eof = kind Token.EOF; diff -r b49366215417 -r 8e8243975860 src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML Fri Jan 17 20:51:36 2014 +0100 +++ b/src/Pure/Isar/token.ML Sat Jan 18 19:15:12 2014 +0100 @@ -8,7 +8,7 @@ sig datatype kind = Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar | - Nat | Float | String | AltString | Verbatim | Space | Comment | InternalValue | + Nat | Float | String | AltString | Verbatim | Cartouche | Space | Comment | InternalValue | Error of string | Sync | EOF type file = {src_path: Path.T, text: string, pos: Position.T} datatype value = @@ -100,7 +100,7 @@ datatype kind = Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar | - Nat | Float | String | AltString | Verbatim | Space | Comment | InternalValue | + Nat | Float | String | AltString | Verbatim | Cartouche | Space | Comment | InternalValue | Error of string | Sync | EOF; datatype T = Token of (Symbol_Pos.text * Position.range) * (kind * string) * slot; @@ -119,6 +119,7 @@ | String => "string" | AltString => "back-quoted string" | Verbatim => "verbatim text" + | Cartouche => "cartouche" | Space => "white space" | Comment => "comment text" | InternalValue => "internal value" @@ -221,6 +222,7 @@ String => Symbol_Pos.quote_string_qq x | AltString => Symbol_Pos.quote_string_bq x | Verbatim => enclose "{*" "*}" x + | Cartouche => cartouche x | Comment => enclose "(*" "*)" x | Sync => "" | EOF => "" @@ -300,16 +302,14 @@ (* scan symbolic idents *) -val is_sym_char = member (op =) (raw_explode "!#$%&*+-/<=>?@^_|~"); - val scan_symid = - Scan.many1 (is_sym_char o Symbol_Pos.symbol) || + Scan.many1 (Symbol.is_symbolic_char o Symbol_Pos.symbol) || Scan.one (Symbol.is_symbolic o Symbol_Pos.symbol) >> single; fun is_symid str = (case try Symbol.explode str of - SOME [s] => Symbol.is_symbolic s orelse is_sym_char s - | SOME ss => forall is_sym_char ss + SOME [s] => Symbol.is_symbolic s orelse Symbol.is_symbolic_char s + | SOME ss => forall Symbol.is_symbolic_char ss | _ => false); fun ident_or_symbolic "begin" = false @@ -333,6 +333,12 @@ $$$ "{" @@@ $$$ "*" @@@ (Scan.repeat scan_verb >> flat); +(* scan cartouche *) + +val scan_cartouche = + Symbol_Pos.scan_pos -- (Symbol_Pos.scan_cartouche_body !!! -- Symbol_Pos.scan_pos); + + (* scan space *) fun space_symbol (s, _) = Symbol.is_blank s andalso s <> "\n"; @@ -367,6 +373,7 @@ (Symbol_Pos.scan_string_qq err_prefix >> token_range String || Symbol_Pos.scan_string_bq err_prefix >> token_range AltString || scan_verbatim >> token_range Verbatim || + scan_cartouche >> token_range Cartouche || scan_comment >> token_range Comment || scan_space >> token Space || Scan.one (Symbol.is_sync o Symbol_Pos.symbol) >> (token Sync o single) || @@ -387,6 +394,7 @@ (Symbol_Pos.recover_string_qq || Symbol_Pos.recover_string_bq || recover_verbatim || + Symbol_Pos.recover_cartouche || Symbol_Pos.recover_comment || Scan.one (Symbol.is_regular o Symbol_Pos.symbol) >> single) >> (single o token (Error msg)); diff -r b49366215417 -r 8e8243975860 src/Pure/Isar/token.scala --- a/src/Pure/Isar/token.scala Fri Jan 17 20:51:36 2014 +0100 +++ b/src/Pure/Isar/token.scala Sat Jan 18 19:15:12 2014 +0100 @@ -26,6 +26,7 @@ val STRING = Value("string") val ALT_STRING = Value("back-quoted string") val VERBATIM = Value("verbatim text") + val CARTOUCHE = Value("cartouche") val SPACE = Value("white space") val COMMENT = Value("comment text") val ERROR = Value("bad input") @@ -74,6 +75,7 @@ kind == Token.Kind.STRING || kind == Token.Kind.ALT_STRING || kind == Token.Kind.VERBATIM || + kind == Token.Kind.CARTOUCHE || kind == Token.Kind.COMMENT def is_ident: Boolean = kind == Token.Kind.IDENT def is_sym_ident: Boolean = kind == Token.Kind.SYM_IDENT @@ -107,6 +109,7 @@ if (kind == Token.Kind.STRING) Scan.Lexicon.empty.quoted_content("\"", source) else if (kind == Token.Kind.ALT_STRING) Scan.Lexicon.empty.quoted_content("`", source) else if (kind == Token.Kind.VERBATIM) Scan.Lexicon.empty.verbatim_content(source) + else if (kind == Token.Kind.CARTOUCHE) Scan.Lexicon.empty.cartouche_content(source) else if (kind == Token.Kind.COMMENT) Scan.Lexicon.empty.comment_content(source) else source diff -r b49366215417 -r 8e8243975860 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Fri Jan 17 20:51:36 2014 +0100 +++ b/src/Pure/PIDE/markup.ML Sat Jan 18 19:15:12 2014 +0100 @@ -59,6 +59,7 @@ val literalN: string val literal: T val delimiterN: string val delimiter: T val inner_stringN: string val inner_string: T + val inner_cartoucheN: string val inner_cartouche: T val inner_commentN: string val inner_comment: T val token_rangeN: string val token_range: T val sortN: string val sort: T @@ -92,6 +93,7 @@ val stringN: string val string: T val altstringN: string val altstring: T val verbatimN: string val verbatim: T + val cartoucheN: string val cartouche: T val commentN: string val comment: T val controlN: string val control: T val tokenN: string val token: Properties.T -> T @@ -307,6 +309,7 @@ val (literalN, literal) = markup_elem "literal"; val (delimiterN, delimiter) = markup_elem "delimiter"; val (inner_stringN, inner_string) = markup_elem "inner_string"; +val (inner_cartoucheN, inner_cartouche) = markup_elem "inner_cartouche"; val (inner_commentN, inner_comment) = markup_elem "inner_comment"; val (token_rangeN, token_range) = markup_elem "token_range"; @@ -361,6 +364,7 @@ val (stringN, string) = markup_elem "string"; val (altstringN, altstring) = markup_elem "altstring"; val (verbatimN, verbatim) = markup_elem "verbatim"; +val (cartoucheN, cartouche) = markup_elem "cartouche"; val (commentN, comment) = markup_elem "comment"; val (controlN, control) = markup_elem "control"; diff -r b49366215417 -r 8e8243975860 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Fri Jan 17 20:51:36 2014 +0100 +++ b/src/Pure/PIDE/markup.scala Sat Jan 18 19:15:12 2014 +0100 @@ -133,6 +133,7 @@ val LITERAL = "literal" val DELIMITER = "delimiter" val INNER_STRING = "inner_string" + val INNER_CARTOUCHE = "inner_cartouche" val INNER_COMMENT = "inner_comment" val TOKEN_RANGE = "token_range" @@ -190,6 +191,7 @@ val STRING = "string" val ALTSTRING = "altstring" val VERBATIM = "verbatim" + val CARTOUCHE = "cartouche" val COMMENT = "comment" val CONTROL = "control" diff -r b49366215417 -r 8e8243975860 src/Pure/Syntax/lexicon.ML --- a/src/Pure/Syntax/lexicon.ML Fri Jan 17 20:51:36 2014 +0100 +++ b/src/Pure/Syntax/lexicon.ML Sat Jan 18 19:15:12 2014 +0100 @@ -25,7 +25,7 @@ val is_tid: string -> bool datatype token_kind = Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | - NumSy | FloatSy | XNumSy | StrSy | Space | Comment | EOF + NumSy | FloatSy | XNumSy | StrSy | Cartouche | Space | Comment | EOF datatype token = Token of token_kind * string * Position.range val str_of_token: token -> string val pos_of_token: token -> Position.T @@ -120,7 +120,7 @@ datatype token_kind = Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | - NumSy | FloatSy | XNumSy | StrSy | Space | Comment | EOF; + NumSy | FloatSy | XNumSy | StrSy | Cartouche | Space | Comment | EOF; datatype token = Token of token_kind * string * Position.range; @@ -160,7 +160,8 @@ ("num_token", NumSy), ("float_token", FloatSy), ("xnum_token", XNumSy), - ("str_token", StrSy)]; + ("str_token", StrSy), + ("cartouche", Cartouche)]; val terminals = map #1 terminal_kinds; val is_terminal = member (op =) terminals; @@ -175,13 +176,14 @@ val token_kind_markup = fn TFreeSy => Markup.tfree - | TVarSy => Markup.tvar - | NumSy => Markup.numeral + | TVarSy => Markup.tvar + | NumSy => Markup.numeral | FloatSy => Markup.numeral - | XNumSy => Markup.numeral - | StrSy => Markup.inner_string + | XNumSy => Markup.numeral + | StrSy => Markup.inner_string + | Cartouche => Markup.inner_cartouche | Comment => Markup.inner_comment - | _ => Markup.empty; + | _ => Markup.empty; fun report_of_token (Token (kind, s, (pos, _))) = let val markup = if kind = Literal then literal_markup s else token_kind_markup kind @@ -267,6 +269,7 @@ val scan_lit = Scan.literal lex >> token Literal; val scan_token = + Symbol_Pos.scan_cartouche !!! >> token Cartouche || Symbol_Pos.scan_comment !!! >> token Comment || Scan.max token_leq scan_lit scan_val || scan_str >> token StrSy || diff -r b49366215417 -r 8e8243975860 src/Pure/Thy/html.ML --- a/src/Pure/Thy/html.ML Fri Jan 17 20:51:36 2014 +0100 +++ b/src/Pure/Thy/html.ML Sat Jan 18 19:15:12 2014 +0100 @@ -188,6 +188,8 @@ ("\\", (3, "<->")), ("\\", (3, "-->")), ("\\", (2, "->")), + ("\\", (1, "‹")), + ("\\", (1, "›")), ("\\<^bsub>", (0, hidden "⇘" ^ "")), ("\\<^esub>", (0, hidden "⇙" ^ "")), ("\\<^bsup>", (0, hidden "⇗" ^ "")), diff -r b49366215417 -r 8e8243975860 src/Pure/Thy/latex.ML --- a/src/Pure/Thy/latex.ML Fri Jan 17 20:51:36 2014 +0100 +++ b/src/Pure/Thy/latex.ML Sat Jan 18 19:15:12 2014 +0100 @@ -125,6 +125,8 @@ val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos); val out = implode (map output_syms_antiq ants); in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end + else if Token.is_kind Token.Cartouche tok then + enclose "{\\isacartoucheopen}" "{\\isacartoucheclose}" (output_syms s) else output_syms s end; diff -r b49366215417 -r 8e8243975860 src/Pure/Thy/thy_syntax.ML --- a/src/Pure/Thy/thy_syntax.ML Fri Jan 17 20:51:36 2014 +0100 +++ b/src/Pure/Thy/thy_syntax.ML Sat Jan 18 19:15:12 2014 +0100 @@ -56,6 +56,7 @@ | Token.String => (Markup.string, "") | Token.AltString => (Markup.altstring, "") | Token.Verbatim => (Markup.verbatim, "") + | Token.Cartouche => (Markup.cartouche, "") | Token.Space => (Markup.empty, "") | Token.Comment => (Markup.comment, "") | Token.InternalValue => (Markup.empty, "") diff -r b49366215417 -r 8e8243975860 src/Pure/library.ML --- a/src/Pure/library.ML Fri Jan 17 20:51:36 2014 +0100 +++ b/src/Pure/library.ML Sat Jan 18 19:15:12 2014 +0100 @@ -139,6 +139,7 @@ val enclose: string -> string -> string -> string val unenclose: string -> string val quote: string -> string + val cartouche: string -> string val space_implode: string -> string list -> string val commas: string list -> string val commas_quote: string list -> string @@ -729,6 +730,8 @@ (*simple quoting (does not escape special chars)*) val quote = enclose "\"" "\""; +val cartouche = enclose "\\" "\\"; + fun space_implode a bs = implode (separate a bs); val commas = space_implode ", "; diff -r b49366215417 -r 8e8243975860 src/Pure/library.scala --- a/src/Pure/library.scala Fri Jan 17 20:51:36 2014 +0100 +++ b/src/Pure/library.scala Sat Jan 18 19:15:12 2014 +0100 @@ -110,6 +110,9 @@ def try_unprefix(prfx: String, s: String): Option[String] = if (s.startsWith(prfx)) Some(s.substring(prfx.length)) else None + def try_unsuffix(sffx: String, s: String): Option[String] = + if (s.endsWith(sffx)) Some(s.substring(0, s.length - sffx.length)) else None + def trim_line(s: String): String = if (s.endsWith("\r\n")) s.substring(0, s.length - 2) else if (s.endsWith("\r") || s.endsWith("\n")) s.substring(0, s.length - 1) diff -r b49366215417 -r 8e8243975860 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Fri Jan 17 20:51:36 2014 +0100 +++ b/src/Pure/pure_thy.ML Sat Jan 18 19:15:12 2014 +0100 @@ -71,7 +71,7 @@ "any", "prop'", "num_const", "float_const", "xnum_const", "num_position", "float_position", "xnum_position", "index", "struct", "tid_position", "tvar_position", "id_position", "longid_position", "var_position", "str_position", - "type_name", "class_name"])) + "cartouche_position", "type_name", "class_name"])) #> Sign.add_syntax_i (map (fn x => (x, typ "'a", NoSyn)) token_markers) #> Sign.add_syntax_i [("", typ "prop' => prop", Delimfix "_"), @@ -155,6 +155,7 @@ ("_position", typ "longid => longid_position", Delimfix "_"), ("_position", typ "var => var_position", Delimfix "_"), ("_position", typ "str_token => str_position", Delimfix "_"), + ("_position", typ "cartouche => cartouche_position", Delimfix "_"), ("_type_constraint_", typ "'a", NoSyn), ("_context_const", typ "id_position => logic", Delimfix "CONST _"), ("_context_const", typ "id_position => aprop", Delimfix "CONST _"), diff -r b49366215417 -r 8e8243975860 src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Fri Jan 17 20:51:36 2014 +0100 +++ b/src/Tools/jEdit/etc/options Sat Jan 18 19:15:12 2014 +0100 @@ -92,6 +92,7 @@ option var_color : string = "00009BFF" option inner_numeral_color : string = "FF0000FF" option inner_quoted_color : string = "D2691EFF" +option inner_cartouche_color : string = "CC6600FF" option inner_comment_color : string = "8B0000FF" option dynamic_color : string = "7BA428FF" diff -r b49366215417 -r 8e8243975860 src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Fri Jan 17 20:51:36 2014 +0100 +++ b/src/Tools/jEdit/src/rendering.scala Sat Jan 18 19:15:12 2014 +0100 @@ -99,6 +99,7 @@ Token.Kind.STRING -> LITERAL1, Token.Kind.ALT_STRING -> LITERAL2, Token.Kind.VERBATIM -> COMMENT3, + Token.Kind.CARTOUCHE -> COMMENT4, Token.Kind.SPACE -> NULL, Token.Kind.COMMENT -> COMMENT1, Token.Kind.ERROR -> INVALID @@ -156,6 +157,7 @@ val var_color = color_value("var_color") val inner_numeral_color = color_value("inner_numeral_color") val inner_quoted_color = color_value("inner_quoted_color") + val inner_cartouche_color = color_value("inner_cartouche_color") val inner_comment_color = color_value("inner_comment_color") val dynamic_color = color_value("dynamic_color") @@ -593,6 +595,7 @@ Markup.BOUND -> bound_color, Markup.VAR -> var_color, Markup.INNER_STRING -> inner_quoted_color, + Markup.INNER_CARTOUCHE -> inner_cartouche_color, Markup.INNER_COMMENT -> inner_comment_color, Markup.DYNAMIC_FACT -> dynamic_color, Markup.ML_KEYWORD -> keyword1_color,