diff --git a/etc/symbols b/etc/symbols --- a/etc/symbols +++ b/etc/symbols @@ -1,429 +1,429 @@ # Default interpretation of some Isabelle symbols \ code: 0x01d7ec group: digit \ code: 0x01d7ed group: digit \ code: 0x01d7ee group: digit \ code: 0x01d7ef group: digit \ code: 0x01d7f0 group: digit \ code: 0x01d7f1 group: digit \ code: 0x01d7f2 group: digit \ code: 0x01d7f3 group: digit \ code: 0x01d7f4 group: digit \ code: 0x01d7f5 group: digit \ code: 0x01d49c group: letter \ code: 0x00212c group: letter \ code: 0x01d49e group: letter \ code: 0x01d49f group: letter \ code: 0x002130 group: letter \ code: 0x002131 group: letter \ code: 0x01d4a2 group: letter \ code: 0x00210b group: letter \ code: 0x002110 group: letter \ code: 0x01d4a5 group: letter \ code: 0x01d4a6 group: letter \ code: 0x002112 group: letter \ code: 0x002133 group: letter \ code: 0x01d4a9 group: letter \ code: 0x01d4aa group: letter \

code: 0x01d5c9 group: letter \ code: 0x01d5ca group: letter \ code: 0x01d5cb group: letter \ code: 0x01d5cc group: letter \ code: 0x01d5cd group: letter \ code: 0x01d5ce group: letter \ code: 0x01d5cf group: letter \ code: 0x01d5d0 group: letter \ code: 0x01d5d1 group: letter \ code: 0x01d5d2 group: letter \ code: 0x01d5d3 group: letter \ code: 0x01d504 group: letter \ code: 0x01d505 group: letter \ code: 0x00212d group: letter \

code: 0x01d507 group: letter \ code: 0x01d508 group: letter \ code: 0x01d509 group: letter \ code: 0x01d50a group: letter \ code: 0x00210c group: letter \ code: 0x002111 group: letter \ code: 0x01d50d group: letter \ code: 0x01d50e group: letter \ code: 0x01d50f group: letter \ code: 0x01d510 group: letter \ code: 0x01d511 group: letter \ code: 0x01d512 group: letter \ code: 0x01d513 group: letter \ code: 0x01d514 group: letter \ code: 0x00211c group: letter \ code: 0x01d516 group: letter \ code: 0x01d517 group: letter \ code: 0x01d518 group: letter \ code: 0x01d519 group: letter \ code: 0x01d51a group: letter \ code: 0x01d51b group: letter \ code: 0x01d51c group: letter \ code: 0x002128 group: letter \ code: 0x01d51e group: letter \ code: 0x01d51f group: letter \ code: 0x01d520 group: letter \
code: 0x01d521 group: letter \ code: 0x01d522 group: letter \ code: 0x01d523 group: letter \ code: 0x01d524 group: letter \ code: 0x01d525 group: letter \ code: 0x01d526 group: letter \ code: 0x01d527 group: letter \ code: 0x01d528 group: letter \ code: 0x01d529 group: letter \ code: 0x01d52a group: letter \ code: 0x01d52b group: letter \ code: 0x01d52c group: letter \ code: 0x01d52d group: letter \ code: 0x01d52e group: letter \ code: 0x01d52f group: letter \ code: 0x01d530 group: letter \ code: 0x01d531 group: letter \ code: 0x01d532 group: letter \ code: 0x01d533 group: letter \ code: 0x01d534 group: letter \ code: 0x01d535 group: letter \ code: 0x01d536 group: letter \ code: 0x01d537 group: letter \ code: 0x0003b1 group: greek \ code: 0x0003b2 group: greek \ code: 0x0003b3 group: greek \ code: 0x0003b4 group: greek \ code: 0x0003b5 group: greek \ code: 0x0003b6 group: greek \ code: 0x0003b7 group: greek \ code: 0x0003b8 group: greek \ code: 0x0003b9 group: greek \ code: 0x0003ba group: greek \ code: 0x0003bb group: greek abbrev: % \ code: 0x0003bc group: greek \ code: 0x0003bd group: greek \ code: 0x0003be group: greek \ code: 0x0003c0 group: greek \ code: 0x0003c1 group: greek \ code: 0x0003c3 group: greek \ code: 0x0003c4 group: greek \ code: 0x0003c5 group: greek \ code: 0x0003c6 group: greek \ code: 0x0003c7 group: greek \ code: 0x0003c8 group: greek \ code: 0x0003c9 group: greek \ code: 0x000393 group: greek \ code: 0x000394 group: greek \ code: 0x000398 group: greek \ code: 0x00039b group: greek \ code: 0x00039e group: greek \ code: 0x0003a0 group: greek \ code: 0x0003a3 group: greek \ code: 0x0003a5 group: greek \ code: 0x0003a6 group: greek \ code: 0x0003a8 group: greek \ code: 0x0003a9 group: greek \ code: 0x01d539 group: letter \ code: 0x002102 group: letter \ code: 0x002115 group: letter \ code: 0x00211a group: letter \ code: 0x00211d group: letter \ code: 0x002124 group: letter \ code: 0x002190 group: arrow abbrev: <. \ code: 0x0027f5 group: arrow abbrev: <. \ code: 0x00290e group: arrow abbrev: <. \ code: 0x0021e0 group: arrow abbrev: <. \ code: 0x002192 group: arrow abbrev: .> abbrev: -> \ code: 0x0027f6 group: arrow abbrev: .> abbrev: --> \ code: 0x00290f group: arrow abbrev: .> abbrev: ---> \ code: 0x0021e2 group: arrow abbrev: .> abbrev: ---> \ code: 0x0021d0 group: arrow abbrev: <. \ code: 0x0027f8 group: arrow abbrev: <. \ code: 0x0021da group: arrow abbrev: <. \ code: 0x0021d2 group: arrow abbrev: .> abbrev: => \ code: 0x0027f9 group: arrow abbrev: .> abbrev: ==> \ code: 0x0021db group: arrow abbrev: .> \ code: 0x002194 group: arrow abbrev: <> abbrev: <-> \ code: 0x0027f7 group: arrow abbrev: <> abbrev: <-> abbrev: <--> \ code: 0x0021d4 group: arrow abbrev: <> \ code: 0x0027fa group: arrow abbrev: <> \ code: 0x0021a6 group: arrow abbrev: .> abbrev: |-> \ code: 0x0027fc group: arrow abbrev: .> abbrev: |--> \ code: 0x002500 group: arrow abbrev: <> \ code: 0x002550 group: arrow abbrev: <> \ code: 0x0021a9 group: arrow abbrev: <. \ code: 0x0021aa group: arrow abbrev: .> \ code: 0x0021bd group: arrow abbrev: <. \ code: 0x0021c1 group: arrow abbrev: .> \ code: 0x0021bc group: arrow abbrev: <. \ code: 0x0021c0 group: arrow abbrev: .> \ code: 0x0021cc group: arrow abbrev: <> abbrev: == \ code: 0x00219d group: arrow abbrev: .> abbrev: ~> \ code: 0x0021c3 group: arrow \ code: 0x0021c2 group: arrow \ code: 0x0021bf group: arrow #\ code: 0x0021be group: arrow \ code: 0x0021be group: operator \ code: 0x002237 group: punctuation \ code: 0x002191 group: arrow \ code: 0x0021d1 group: arrow \ code: 0x002193 group: arrow \ code: 0x0021d3 group: arrow \ code: 0x002195 group: arrow \ code: 0x0021d5 group: arrow \ code: 0x0027e8 group: punctuation abbrev: << \ code: 0x0027e9 group: punctuation abbrev: >> \ code: 0x002308 group: punctuation abbrev: [. \ code: 0x002309 group: punctuation abbrev: .] \ code: 0x00230a group: punctuation abbrev: [. \ code: 0x00230b group: punctuation abbrev: .] \ code: 0x002987 group: punctuation abbrev: (| \ code: 0x002988 group: punctuation abbrev: |) \ code: 0x0027e6 group: punctuation abbrev: [| \ code: 0x0027e7 group: punctuation abbrev: |] \ code: 0x002983 group: punctuation abbrev: {| \ code: 0x002984 group: punctuation abbrev: |} \ code: 0x0000ab group: punctuation abbrev: << \ code: 0x0000bb group: punctuation abbrev: >> \ code: 0x0022a5 group: logic \ code: 0x0022a4 group: logic \ code: 0x002227 group: logic abbrev: /\ abbrev: & \ code: 0x0022c0 group: logic abbrev: !! \ code: 0x002228 group: logic abbrev: \/ abbrev: | \ code: 0x0022c1 group: logic abbrev: ?? \ code: 0x002200 group: logic abbrev: ! abbrev: ALL \ code: 0x002203 group: logic abbrev: ? abbrev: EX \ code: 0x002204 group: logic abbrev: ~? \ code: 0x0000ac group: logic abbrev: ~ \ code: 0x0025cb group: logic \ code: 0x0025a1 group: logic \ code: 0x0025c7 group: logic \ code: 0x0022c4 group: operator \ code: 0x0022a2 group: relation abbrev: |- \ code: 0x0022a8 group: relation abbrev: |= \ code: 0x0022a9 group: relation abbrev: |- \ code: 0x0022ab group: relation abbrev: |= \ code: 0x0022a3 group: relation abbrev: -| \ code: 0x00221a group: relation \ code: 0x002264 group: relation abbrev: <= \ code: 0x002265 group: relation abbrev: >= \ code: 0x00226a group: relation abbrev: << \ code: 0x00226b group: relation abbrev: >> \ code: 0x002272 group: relation \ code: 0x002273 group: relation \ code: 0x002a85 group: relation \ code: 0x002a86 group: relation \ code: 0x002208 group: relation abbrev: : \ code: 0x002209 group: relation abbrev: ~: \ code: 0x002282 group: relation \ code: 0x002283 group: relation \ code: 0x002286 group: relation abbrev: (= \ code: 0x002287 group: relation abbrev: )= \ code: 0x00228f group: relation \ code: 0x002290 group: relation \ code: 0x002291 group: relation abbrev: [= \ code: 0x002292 group: relation abbrev: ]= \ code: 0x002229 group: operator abbrev: Int \ code: 0x0022c2 group: operator abbrev: Inter abbrev: INT \ code: 0x00222a group: operator abbrev: Un \ code: 0x0022c3 group: operator abbrev: Union abbrev: UN \ code: 0x002294 group: operator \ code: 0x002a06 group: operator abbrev: SUP \ code: 0x002293 group: operator \ code: 0x002a05 group: operator abbrev: INF \ code: 0x002216 group: operator \ code: 0x00221d group: operator \ code: 0x00228e group: operator \ code: 0x002a04 group: operator \ code: 0x002260 group: relation abbrev: ~= \ code: 0x00223c group: relation \ code: 0x002250 group: relation abbrev: .= \ code: 0x002243 group: relation \ code: 0x002248 group: relation \ code: 0x00224d group: relation \ code: 0x002245 group: relation \ code: 0x002323 group: relation \ code: 0x002261 group: relation abbrev: == \ code: 0x002322 group: relation \ code: 0x0022c8 \ code: 0x002a1d \ code: 0x00227a group: relation \ code: 0x00227b group: relation \ code: 0x00227c group: relation \ code: 0x00227d group: relation \ code: 0x002225 group: punctuation abbrev: || \ code: 0x0000a6 group: punctuation abbrev: || \ code: 0x0000b1 group: operator \ code: 0x002213 group: operator \ code: 0x0000d7 group: operator abbrev: <*> \
code: 0x0000f7 group: operator \ code: 0x0022c5 group: operator \ code: 0x0022c6 group: operator \ code: 0x002219 group: operator \ code: 0x002218 group: operator \ code: 0x002020 \ code: 0x002021 \ code: 0x0022b2 group: relation \ code: 0x0022b3 group: relation \ code: 0x0022b4 group: relation \ code: 0x0022b5 group: relation \ code: 0x0025c3 group: relation \ code: 0x0025b9 group: relation \ code: 0x0025b3 group: relation \ code: 0x00225c group: relation \ code: 0x002295 group: operator \ code: 0x002a01 group: operator \ code: 0x002297 group: operator \ code: 0x002a02 group: operator \ code: 0x002299 group: operator \ code: 0x002a00 group: operator \ code: 0x002296 group: operator \ code: 0x002298 group: operator \ code: 0x002026 group: punctuation abbrev: ... \ code: 0x0022ef group: punctuation \ code: 0x002211 group: operator abbrev: SUM \ code: 0x00220f group: operator abbrev: PROD \ code: 0x002210 group: operator \ code: 0x00221e \ code: 0x00222b group: operator \ code: 0x00222e group: operator \ code: 0x002663 \ code: 0x002662 \ code: 0x002661 \ code: 0x002660 \ code: 0x002135 \ code: 0x002205 \ code: 0x002207 \ code: 0x002202 \ code: 0x00266d \ code: 0x00266e \ code: 0x00266f \ code: 0x002220 \ code: 0x0000a9 \ code: 0x0000ae \ code: 0x002010 group: punctuation \ code: 0x0000af group: operator \ code: 0x0000bc group: digit \ code: 0x0000bd group: digit \ code: 0x0000be group: digit \ code: 0x0000aa \ code: 0x0000ba \
code: 0x0000a7 \ code: 0x0000b6 \ code: 0x0000a1 \ code: 0x0000bf \ code: 0x0020ac \ code: 0x0000a3 \ code: 0x0000a5 \ code: 0x0000a2 \ code: 0x0000a4 \ code: 0x0000b0 \ code: 0x002a3f group: operator \ code: 0x002127 group: operator \ code: 0x0025ca \ code: 0x002118 \ code: 0x002240 group: relation \ code: 0x0000b4 \ code: 0x000131 \ code: 0x0000a8 \ code: 0x0000b8 \ code: 0x0002dd \ code: 0x00291c group: operator abbrev: >>= \ code: 0x002aa2 group: operator abbrev: >> \ code: 0x0003f5 \ code: 0x002311 \ code: 0x0023ce \ code: 0x002015 group: document argument: space_cartouche font: Isabelle␣DejaVu␣Sans␣Mono -\ code: 0x002710 group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^cancel> code: 0x002326 group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^latex> group: document argument: cartouche +\<^marker> code: 0x002710 group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \ code: 0x002039 group: punctuation font: Isabelle␣DejaVu␣Sans␣Mono abbrev: << \ code: 0x00203a group: punctuation font: Isabelle␣DejaVu␣Sans␣Mono abbrev: >> \<^here> code: 0x002302 font: Isabelle␣DejaVu␣Sans␣Mono \<^undefined> code: 0x002756 font: Isabelle␣DejaVu␣Sans␣Mono \<^noindent> code: 0x0021e4 group: document font: Isabelle␣DejaVu␣Sans␣Mono \<^smallskip> code: 0x002508 group: document font: Isabelle␣DejaVu␣Sans␣Mono \<^medskip> code: 0x002509 group: document font: Isabelle␣DejaVu␣Sans␣Mono \<^bigskip> code: 0x002501 group: document font: Isabelle␣DejaVu␣Sans␣Mono \<^item> code: 0x0025aa group: document font: Isabelle␣DejaVu␣Sans␣Mono \<^enum> code: 0x0025b8 group: document font: Isabelle␣DejaVu␣Sans␣Mono \<^descr> code: 0x0027a7 group: document font: Isabelle␣DejaVu␣Sans␣Mono \<^footnote> code: 0x00204b group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^verbatim> code: 0x0025a9 group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^theory_text> code: 0x002b1a group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^emph> code: 0x002217 group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^bold> code: 0x002759 group: control argument: cartouche group: document font: Isabelle␣DejaVu␣Sans␣Mono \<^sub> code: 0x0021e9 group: control font: Isabelle␣DejaVu␣Sans␣Mono \<^sup> code: 0x0021e7 group: control font: Isabelle␣DejaVu␣Sans␣Mono \<^bsub> code: 0x0021d8 group: control_block font: Isabelle␣DejaVu␣Sans␣Mono abbrev: =_( \<^esub> code: 0x0021d9 group: control_block font: Isabelle␣DejaVu␣Sans␣Mono abbrev: =_) \<^bsup> code: 0x0021d7 group: control_block font: Isabelle␣DejaVu␣Sans␣Mono abbrev: =^( \<^esup> code: 0x0021d6 group: control_block font: Isabelle␣DejaVu␣Sans␣Mono abbrev: =^) \<^file> code: 0x01F5CF group: icon argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^dir> code: 0x01F5C0 group: icon argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^url> code: 0x01F310 group: icon argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^doc> code: 0x01F4D3 group: icon argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^action> code: 0x00261b group: icon argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^assert> \<^binding> argument: cartouche \<^class> argument: cartouche \<^class_syntax> argument: cartouche \<^command_keyword> argument: cartouche \<^const_abbrev> argument: cartouche \<^const_name> argument: cartouche \<^const_syntax> argument: cartouche \<^context> \<^cprop> argument: cartouche \<^cterm> argument: cartouche \<^ctyp> argument: cartouche \<^keyword> argument: cartouche \<^locale> argument: cartouche \<^make_string> \<^method> argument: cartouche \<^named_theorems> argument: cartouche \<^nonterminal> argument: cartouche \<^path> argument: cartouche \<^plugin> argument: cartouche \<^print> \<^prop> argument: cartouche \<^session> argument: cartouche \<^simproc> argument: cartouche \<^sort> argument: cartouche \<^syntax_const> argument: cartouche \<^system_option> argument: cartouche \<^term> argument: cartouche \<^theory> argument: cartouche \<^theory_context> argument: cartouche \<^typ> argument: cartouche \<^type_abbrev> argument: cartouche \<^type_name> argument: cartouche \<^type_syntax> argument: cartouche \<^code> argument: cartouche \<^computation> argument: cartouche \<^computation_conv> argument: cartouche \<^computation_check> argument: cartouche diff --git a/src/Pure/General/antiquote.ML b/src/Pure/General/antiquote.ML --- a/src/Pure/General/antiquote.ML +++ b/src/Pure/General/antiquote.ML @@ -1,185 +1,185 @@ (* Title: Pure/General/antiquote.ML Author: Makarius Antiquotations within plain text. *) signature ANTIQUOTE = sig type control = {range: Position.range, name: string * Position.T, body: Symbol_Pos.T list} type antiq = {start: Position.T, stop: Position.T, range: Position.range, body: Symbol_Pos.T list} datatype 'a antiquote = Text of 'a | Control of control | Antiq of antiq type text_antiquote = Symbol_Pos.T list antiquote val text_antiquote_range: text_antiquote -> Position.range val text_range: text_antiquote list -> Position.range val split_lines: text_antiquote list -> text_antiquote list list val antiq_reports: 'a antiquote list -> Position.report list val update_reports: bool -> Position.T -> string list -> Position.report_text list val scan_control: control scanner val scan_antiq: antiq scanner val scan_antiquote: text_antiquote scanner val scan_antiquote_comments: text_antiquote scanner val parse_comments: Position.T -> Symbol_Pos.T list -> text_antiquote list val read_comments: Input.source -> text_antiquote list end; structure Antiquote: ANTIQUOTE = struct (* datatype antiquote *) type control = {range: Position.range, name: string * Position.T, body: Symbol_Pos.T list}; type antiq = {start: Position.T, stop: Position.T, range: Position.range, body: Symbol_Pos.T list}; datatype 'a antiquote = Text of 'a | Control of control | Antiq of antiq; type text_antiquote = Symbol_Pos.T list antiquote; fun text_antiquote_range (Text ss) = Symbol_Pos.range ss | text_antiquote_range (Control {range, ...}) = range | text_antiquote_range (Antiq {range, ...}) = range; fun text_range ants = if null ants then Position.no_range else Position.range (#1 (text_antiquote_range (hd ants)), #2 (text_antiquote_range (List.last ants))); (* split lines *) fun split_lines input = let fun add a (line, lines) = (a :: line, lines); fun flush (line, lines) = ([], rev line :: lines); fun split (a as Text ss) = (case chop_prefix (fn ("\n", _) => false | _ => true) ss of ([], []) => I | (_, []) => add a | ([], _ :: rest) => flush #> split (Text rest) | (prefix, _ :: rest) => add (Text prefix) #> flush #> split (Text rest)) | split a = add a; in if null input then [] else rev (#2 (flush (fold split input ([], [])))) end; (* reports *) fun antiq_reports ants = ants |> maps (fn Text _ => [] | Control {range = (pos, _), ...} => [(pos, Markup.antiquoted)] | Antiq {start, stop, range = (pos, _), ...} => [(start, Markup.antiquote), (stop, Markup.antiquote), (pos, Markup.antiquoted), (pos, Markup.language_antiquotation)]); (* update *) fun update_reports embedded pos src = let val n = length src; val no_arg = n = 1; val embedded_arg = n = 2 andalso embedded; val control = (case src of name :: _ => if Symbol.is_ascii_identifier name andalso name <> "cartouche" andalso (no_arg orelse embedded_arg) then SOME (Symbol.control_prefix ^ name ^ Symbol.control_suffix) else NONE | [] => NONE); val arg = if embedded_arg then cartouche (nth src 1) else ""; in (case control of SOME sym => [((pos, Markup.update), sym ^ arg)] | NONE => []) end; (* scan *) open Basic_Symbol_Pos; local val err_prefix = "Antiquotation lexical error: "; val scan_nl = Scan.one (fn (s, _) => s = "\n") >> single; val scan_nl_opt = Scan.optional scan_nl []; val scan_plain_txt = Scan.many1 (fn (s, _) => not (Comment.is_symbol s) andalso not (Symbol.is_control s) andalso s <> Symbol.open_ andalso s <> "@" andalso s <> "\n" andalso Symbol.not_eof s) || Scan.one (Comment.is_symbol o Symbol_Pos.symbol) >> single || $$$ "@" --| Scan.ahead (~$$ "{"); val scan_text = scan_nl || Scan.repeats1 scan_plain_txt @@@ scan_nl_opt; val scan_text_comments = - scan_nl || Scan.repeats1 (Comment.scan >> #2 || scan_plain_txt) @@@ scan_nl_opt; + scan_nl || Scan.repeats1 (Comment.scan_inner >> #2 || scan_plain_txt) @@@ scan_nl_opt; val scan_antiq_body = Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 || Symbol_Pos.scan_cartouche err_prefix || - Comment.scan -- + Comment.scan_inner -- Symbol_Pos.!!! (fn () => err_prefix ^ "bad formal comment in antiquote body") Scan.fail >> K [] || Scan.one (fn (s, _) => s <> "}" andalso Symbol.not_eof s) >> single; fun control_name sym = (case Symbol.decode sym of Symbol.Control name => name); in val scan_control = Scan.option (Scan.one (Symbol.is_control o Symbol_Pos.symbol)) -- Symbol_Pos.scan_cartouche err_prefix >> (fn (opt_control, body) => let val (name, range) = (case opt_control of SOME (sym, pos) => ((control_name sym, pos), Symbol_Pos.range ((sym, pos) :: body)) | NONE => (("cartouche", #2 (hd body)), Symbol_Pos.range body)); in {name = name, range = range, body = body} end) || Scan.one (Symbol.is_control o Symbol_Pos.symbol) >> (fn (sym, pos) => {name = (control_name sym, pos), range = Symbol_Pos.range [(sym, pos)], body = []}); val scan_antiq = Symbol_Pos.scan_pos -- ($$ "@" |-- $$ "{" |-- Symbol_Pos.scan_pos -- Symbol_Pos.!!! (fn () => err_prefix ^ "missing closing brace") (Scan.repeats scan_antiq_body -- Symbol_Pos.scan_pos -- ($$ "}" |-- Symbol_Pos.scan_pos))) >> (fn (pos1, (pos2, ((body, pos3), pos4))) => {start = Position.range_position (pos1, pos2), stop = Position.range_position (pos3, pos4), range = Position.range (pos1, pos4), body = body}); val scan_antiquote = scan_text >> Text || scan_control >> Control || scan_antiq >> Antiq; val scan_antiquote_comments = scan_text_comments >> Text || scan_control >> Control || scan_antiq >> Antiq; end; (* parse and read (with formal comments) *) fun parse_comments pos syms = (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote_comments) syms of SOME ants => ants | NONE => error ("Malformed quotation/antiquotation source" ^ Position.here pos)); fun read_comments source = let val ants = parse_comments (Input.pos_of source) (Input.source_explode source); val _ = Position.reports (antiq_reports ants); in ants end; end; diff --git a/src/Pure/General/comment.ML b/src/Pure/General/comment.ML --- a/src/Pure/General/comment.ML +++ b/src/Pure/General/comment.ML @@ -1,85 +1,93 @@ (* Title: Pure/General/comment.ML Author: Makarius Formal comments. *) signature COMMENT = sig - datatype kind = Comment | Cancel | Latex + datatype kind = Comment | Cancel | Latex | Marker val markups: kind -> Markup.T list val is_symbol: Symbol.symbol -> bool val scan_comment: (kind * Symbol_Pos.T list) scanner val scan_cancel: (kind * Symbol_Pos.T list) scanner val scan_latex: (kind * Symbol_Pos.T list) scanner - val scan: (kind * Symbol_Pos.T list) scanner + val scan_marker: (kind * Symbol_Pos.T list) scanner + val scan_inner: (kind * Symbol_Pos.T list) scanner + val scan_outer: (kind * Symbol_Pos.T list) scanner val read_body: Symbol_Pos.T list -> (kind option * Symbol_Pos.T list) list end; structure Comment: COMMENT = struct (* kinds *) -datatype kind = Comment | Cancel | Latex; +datatype kind = Comment | Cancel | Latex | Marker; val kinds = [(Comment, {symbol = Symbol.comment, blanks = true, markups = [Markup.language_document true]}), (Cancel, {symbol = Symbol.cancel, blanks = false, markups = [Markup.language_text true]}), (Latex, {symbol = Symbol.latex, blanks = false, - markups = [Markup.language_latex true, Markup.no_words]})]; + markups = [Markup.language_latex true, Markup.no_words]}), + (Marker, + {symbol = Symbol.marker, blanks = false, + markups = [Markup.language_document_marker]})]; val get_kind = the o AList.lookup (op =) kinds; val print_kind = quote o #symbol o get_kind; val markups = #markups o get_kind; fun is_symbol sym = exists (fn (_, {symbol, ...}) => symbol = sym) kinds; (* scan *) local open Basic_Symbol_Pos; val err_prefix = "Error in formal comment: "; val scan_blanks = Scan.many (Symbol.is_blank o Symbol_Pos.symbol); fun scan_symbol kind = let val {blanks, symbol, ...} = get_kind kind in if blanks then $$$ symbol @@@ scan_blanks else $$$ symbol end; fun scan_strict kind = scan_symbol kind @@@ Symbol_Pos.!!! (fn () => err_prefix ^ "cartouche expected after " ^ print_kind kind) (Symbol_Pos.scan_cartouche err_prefix) >> pair kind; fun scan_permissive kind = scan_symbol kind -- Scan.option (Symbol_Pos.scan_cartouche err_prefix) >> (fn (ss, NONE) => (NONE, ss) | (_, SOME ss) => (SOME kind, ss)); in val scan_comment = scan_strict Comment; val scan_cancel = scan_strict Cancel; val scan_latex = scan_strict Latex; -val scan = scan_comment || scan_cancel || scan_latex; +val scan_marker = scan_strict Marker; + +val scan_inner = scan_comment || scan_cancel || scan_latex; +val scan_outer = scan_inner || scan_marker; val scan_body = Scan.many1 (fn (s, _) => not (is_symbol s) andalso Symbol.not_eof s) >> pair NONE || scan_permissive Comment || scan_permissive Cancel || scan_permissive Latex; fun read_body syms = (if exists (is_symbol o Symbol_Pos.symbol) syms then Scan.read Symbol_Pos.stopper (Scan.repeat scan_body) syms else NONE) |> the_default [(NONE, syms)]; end; end; diff --git a/src/Pure/General/comment.scala b/src/Pure/General/comment.scala --- a/src/Pure/General/comment.scala +++ b/src/Pure/General/comment.scala @@ -1,72 +1,74 @@ /* Title: Pure/General/comment.scala Author: Makarius Formal comments. */ package isabelle object Comment { object Kind extends Enumeration { val COMMENT = Value("formal comment") val CANCEL = Value("canceled text") val LATEX = Value("embedded LaTeX") + val MARKER = Value("document marker") } lazy val symbols: Set[Symbol.Symbol] = Set(Symbol.comment, Symbol.comment_decoded, Symbol.cancel, Symbol.cancel_decoded, - Symbol.latex, Symbol.latex_decoded) + Symbol.latex, Symbol.latex_decoded, + Symbol.marker, Symbol.marker_decoded) lazy val symbols_blanks: Set[Symbol.Symbol] = Set(Symbol.comment, Symbol.comment_decoded) def content(source: String): String = { def err(): Nothing = error("Malformed formal comment: " + quote(source)) Symbol.explode(source) match { case sym :: rest if symbols_blanks(sym) => val body = if (symbols_blanks(sym)) rest.dropWhile(Symbol.is_blank) else rest try { Scan.Parsers.cartouche_content(body.mkString) } catch { case ERROR(_) => err() } case _ => err() } } trait Parsers extends Scan.Parsers { def comment_prefix: Parser[String] = one(symbols_blanks) ~ many(Symbol.is_blank) ^^ { case a ~ b => a + b.mkString } | one(symbols) def comment_cartouche: Parser[String] = comment_prefix ~ cartouche ^^ { case a ~ b => a + b } def comment_cartouche_line(ctxt: Scan.Line_Context): Parser[(String, Scan.Line_Context)] = { def cartouche_context(d: Int): Scan.Line_Context = if (d == 0) Scan.Finished else Scan.Cartouche_Comment(d) ctxt match { case Scan.Finished => comment_prefix ~ opt(cartouche_depth(0)) ^^ { case a ~ None => (a, Scan.Comment_Prefix(a)) case a ~ Some((c, d)) => (a + c, cartouche_context(d)) } case Scan.Comment_Prefix(a) if symbols_blanks(a) => many1(Symbol.is_blank) ~ opt(cartouche_depth(0)) ^^ { case b ~ None => (b.mkString, Scan.Comment_Prefix(a)) case b ~ Some((c, d)) => (b.mkString + c, cartouche_context(d)) } | cartouche_depth(0) ^^ { case (c, d) => (c, cartouche_context(d)) } case Scan.Comment_Prefix(_) => cartouche_depth(0) ^^ { case (c, d) => (c, cartouche_context(d)) } case Scan.Cartouche_Comment(depth) => cartouche_depth(depth) ^^ { case (c, d) => (c, cartouche_context(d)) } case _ => failure("") } } } } diff --git a/src/Pure/General/symbol.ML b/src/Pure/General/symbol.ML --- a/src/Pure/General/symbol.ML +++ b/src/Pure/General/symbol.ML @@ -1,516 +1,518 @@ (* Title: Pure/General/symbol.ML Author: Makarius Isabelle text symbols. *) signature SYMBOL = sig type symbol = string val explode: string -> symbol list val spaces: int -> string val STX: symbol val DEL: symbol val open_: symbol val close: symbol val space: symbol val is_space: symbol -> bool val comment: symbol val cancel: symbol val latex: symbol + val marker: symbol 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 control_prefix: string val control_suffix: string val is_control: symbol -> bool val eof: symbol val is_eof: symbol -> bool val not_eof: symbol -> bool val stopper: symbol Scan.stopper val is_malformed: symbol -> bool val malformed_msg: symbol -> string val is_ascii: symbol -> bool val is_ascii_letter: symbol -> bool val is_ascii_digit: symbol -> bool val is_ascii_hex: symbol -> bool val is_ascii_quasi: symbol -> bool val is_ascii_blank: symbol -> bool val is_ascii_line_terminator: symbol -> bool val is_ascii_control: symbol -> bool val is_ascii_letdig: symbol -> bool val is_ascii_lower: symbol -> bool val is_ascii_upper: symbol -> bool val to_ascii_lower: symbol -> symbol val to_ascii_upper: symbol -> symbol val is_ascii_identifier: string -> bool val scan_ascii_id: string list -> string * string list datatype sym = Char of string | UTF8 of string | Sym of string | Control of string | Malformed of string | EOF val decode: symbol -> sym val encode: sym -> symbol datatype kind = Letter | Digit | Quasi | Blank | Other val kind: symbol -> kind val is_letter: symbol -> bool val is_digit: symbol -> bool val is_quasi: symbol -> bool val is_blank: symbol -> bool val is_block_ctrl: symbol -> bool val is_quasi_letter: symbol -> bool val is_letdig: symbol -> bool val beginning: int -> symbol list -> string val esc: symbol -> string val escape: string -> string val scanner: string -> (string list -> 'a * string list) -> symbol list -> 'a val split_words: symbol list -> string list val explode_words: string -> string list val trim_blanks: string -> string val bump_init: string -> string val bump_string: string -> string val sub: symbol val sup: symbol val bold: symbol val make_sub: string -> string val make_sup: string -> string val make_bold: string -> string val length: symbol list -> int val output: string -> Output.output * int end; structure Symbol: SYMBOL = struct (** type symbol **) (*Symbols, which are considered the smallest entities of any Isabelle string, may be of the following form: (1) ASCII: a (2) UTF-8: ä (2) regular symbols: \ (3) control symbols: \<^ident> Output is subject to the print_mode variable (default: verbatim), actual interpretation in display is up to front-end tools. *) type symbol = string; val STX = chr 2; val DEL = chr 127; val open_ = "\"; val close = "\"; val space = chr 32; fun is_space s = s = space; local val small_spaces = Vector.tabulate (65, fn i => replicate_string i space); in fun spaces n = if n < 64 then Vector.sub (small_spaces, n) else replicate_string (n div 64) (Vector.sub (small_spaces, 64)) ^ Vector.sub (small_spaces, n mod 64); end; val comment = "\"; val cancel = "\<^cancel>"; val latex = "\<^latex>"; +val marker = "\<^marker>"; fun is_char s = size s = 1; fun is_utf8 s = size s > 0 andalso forall_string (fn c => ord c >= 128) s; fun raw_symbolic s = String.isPrefix "\092<" s andalso String.isSuffix ">" s andalso not (String.isPrefix "\092<^" s); fun is_symbolic s = s <> open_ andalso s <> close andalso raw_symbolic s; val is_symbolic_char = member (op =) (raw_explode "!#$%&*+-/<=>?@^_|~"); fun is_printable s = if is_char s then 32 <= ord s andalso ord s <= Char.ord #"~" else is_utf8 s orelse raw_symbolic s; val control_prefix = "\092<^"; val control_suffix = ">"; fun is_control s = String.isPrefix control_prefix s andalso String.isSuffix control_suffix s; (* input source control *) val eof = ""; fun is_eof s = s = eof; fun not_eof s = s <> eof; val stopper = Scan.stopper (K eof) is_eof; fun is_malformed s = String.isPrefix "\092<" s andalso not (String.isSuffix ">" s) orelse s = "\092<>" orelse s = "\092<^>"; fun malformed_msg s = "Malformed symbolic character: " ^ quote s; (* ASCII symbols *) fun is_ascii s = is_char s andalso ord s < 128; fun is_ascii_letter s = is_char s andalso (Char.ord #"A" <= ord s andalso ord s <= Char.ord #"Z" orelse Char.ord #"a" <= ord s andalso ord s <= Char.ord #"z"); fun is_ascii_digit s = is_char s andalso Char.ord #"0" <= ord s andalso ord s <= Char.ord #"9"; fun is_ascii_hex s = is_char s andalso (Char.ord #"0" <= ord s andalso ord s <= Char.ord #"9" orelse Char.ord #"A" <= ord s andalso ord s <= Char.ord #"F" orelse Char.ord #"a" <= ord s andalso ord s <= Char.ord #"f"); fun is_ascii_quasi "_" = true | is_ascii_quasi "'" = true | is_ascii_quasi _ = false; val is_ascii_blank = fn " " => true | "\t" => true | "\n" => true | "\^K" => true | "\f" => true | "\^M" => true | _ => false; val is_ascii_line_terminator = fn "\r" => true | "\n" => true | _ => false; fun is_ascii_control s = is_char s andalso ord s < 32 andalso not (is_ascii_blank s); fun is_ascii_letdig s = is_ascii_letter s orelse is_ascii_digit s orelse is_ascii_quasi s; fun is_ascii_lower s = is_char s andalso (Char.ord #"a" <= ord s andalso ord s <= Char.ord #"z"); fun is_ascii_upper s = is_char s andalso (Char.ord #"A" <= ord s andalso ord s <= Char.ord #"Z"); fun to_ascii_lower s = if is_ascii_upper s then chr (ord s + Char.ord #"a" - Char.ord #"A") else s; fun to_ascii_upper s = if is_ascii_lower s then chr (ord s + Char.ord #"A" - Char.ord #"a") else s; fun is_ascii_identifier s = size s > 0 andalso is_ascii_letter (String.substring (s, 0, 1)) andalso forall_string is_ascii_letdig s; val scan_ascii_id = Scan.one is_ascii_letter ^^ (Scan.many is_ascii_letdig >> implode); (* diagnostics *) fun beginning n cs = let val drop_blanks = drop_suffix is_ascii_blank; val all_cs = drop_blanks cs; val dots = if length all_cs > n then " ..." else ""; in (drop_blanks (take n all_cs) |> map (fn c => if is_ascii_blank c then space else c) |> implode) ^ dots end; (* symbol variants *) datatype sym = Char of string | UTF8 of string | Sym of string | Control of string | Malformed of string | EOF; fun decode s = if s = "" then EOF else if is_char s then Char s else if is_utf8 s then UTF8 s else if is_malformed s then Malformed s else if is_control s then Control (String.substring (s, 3, size s - 4)) else Sym (String.substring (s, 2, size s - 3)); fun encode (Char s) = s | encode (UTF8 s) = s | encode (Sym s) = "\092<" ^ s ^ ">" | encode (Control s) = "\092<^" ^ s ^ ">" | encode (Malformed s) = s | encode EOF = ""; (* standard symbol kinds *) local val letter_symbols = Symtab.make_set [ "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\

", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\

", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\
", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", (*"\", sic!*) "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\" ]; in val is_letter_symbol = Symtab.defined letter_symbols; end; datatype kind = Letter | Digit | Quasi | Blank | Other; fun kind s = if is_ascii_letter s then Letter else if is_ascii_digit s then Digit else if is_ascii_quasi s then Quasi else if is_ascii_blank s then Blank else if is_char s then Other else if is_letter_symbol s then Letter else Other; fun is_letter s = kind s = Letter; fun is_digit s = kind s = Digit; fun is_quasi s = kind s = Quasi; fun is_blank s = kind s = Blank; val is_block_ctrl = member (op =) ["\<^bsub>", "\<^esub>", "\<^bsup>", "\<^esup>"]; fun is_quasi_letter s = let val k = kind s in k = Letter orelse k = Quasi end; fun is_letdig s = let val k = kind s in k = Letter orelse k = Digit orelse k = Quasi end; (* escape *) val esc = fn s => if is_char s then s else if is_utf8 s then translate_string (fn c => "\\" ^ string_of_int (ord c)) s else "\\" ^ s; val escape = implode o map esc o Symbol.explode; (** scanning through symbols **) (* scanner *) fun scanner msg scan syms = let fun message (ss, NONE) = (fn () => msg ^ ": " ^ quote (beginning 10 ss)) | message (ss, SOME msg') = (fn () => msg ^ ", " ^ msg' () ^ ": " ^ quote (beginning 10 ss)); val finite_scan = Scan.error (Scan.finite stopper (!! message scan)); in (case finite_scan syms of (result, []) => result | (_, rest) => error (message (rest, NONE) ())) end; (* space-separated words *) val scan_word = Scan.many1 is_ascii_blank >> K NONE || Scan.many1 (fn s => not (is_ascii_blank s) andalso not_eof s) >> (SOME o implode); val split_words = scanner "Bad text" (Scan.repeat scan_word >> map_filter I); val explode_words = split_words o Symbol.explode; (* blanks *) val trim_blanks = Symbol.explode #> trim is_blank #> implode; (* bump string -- treat as base 26 or base 1 numbers *) fun symbolic_end (_ :: "\<^sub>" :: _) = true | symbolic_end ("'" :: ss) = symbolic_end ss | symbolic_end (s :: _) = raw_symbolic s | symbolic_end [] = false; fun bump_init str = if symbolic_end (rev (Symbol.explode str)) then str ^ "'" else str ^ "a"; fun bump_string str = let fun bump [] = ["a"] | bump ("z" :: ss) = "a" :: bump ss | bump (s :: ss) = if is_char s andalso Char.ord #"a" <= ord s andalso ord s < Char.ord #"z" then chr (ord s + 1) :: ss else "a" :: s :: ss; val (ss, qs) = apfst rev (chop_suffix is_quasi (Symbol.explode str)); val ss' = if symbolic_end ss then "'" :: ss else bump ss; in implode (rev ss' @ qs) end; (* styles *) val sub = "\092<^sub>"; val sup = "\092<^sup>"; val bold = "\092<^bold>"; fun make_style sym = Symbol.explode #> maps (fn s => [sym, s]) #> implode; val make_sub = make_style sub; val make_sup = make_style sup; val make_bold = make_style bold; (** symbol output **) (* length *) fun sym_len s = if not (is_printable s) then (0: int) else if String.isPrefix "\092 fn n => sym_len s + n) ss 0; fun output s = (s, sym_length (Symbol.explode s)); (*final declarations of this structure!*) val explode = Symbol.explode; val length = sym_length; end; diff --git a/src/Pure/General/symbol.scala b/src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala +++ b/src/Pure/General/symbol.scala @@ -1,664 +1,658 @@ /* Title: Pure/General/symbol.scala Author: Makarius Isabelle text symbols. */ package isabelle import scala.collection.mutable import scala.util.matching.Regex import scala.annotation.tailrec object Symbol { type Symbol = String // counting Isabelle symbols, starting from 1 type Offset = Text.Offset type Range = Text.Range /* spaces */ val space = " " private val static_spaces = space * 4000 def spaces(n: Int): String = { require(n >= 0) if (n < static_spaces.length) static_spaces.substring(0, n) else space * n } /* ASCII characters */ def is_ascii_letter(c: Char): Boolean = 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z' def is_ascii_digit(c: Char): Boolean = '0' <= c && c <= '9' def is_ascii_hex(c: Char): Boolean = '0' <= c && c <= '9' || 'A' <= c && c <= 'F' || 'a' <= c && c <= 'f' def is_ascii_quasi(c: Char): Boolean = c == '_' || c == '\'' def is_ascii_blank(c: Char): Boolean = " \t\n\u000b\f\r".contains(c) def is_ascii_line_terminator(c: Char): Boolean = "\r\n".contains(c) def is_ascii_letdig(c: Char): Boolean = is_ascii_letter(c) || is_ascii_digit(c) || is_ascii_quasi(c) def is_ascii_identifier(s: String): Boolean = s.length > 0 && is_ascii_letter(s(0)) && s.forall(is_ascii_letdig) def ascii(c: Char): Symbol = { if (c > 127) error("Non-ASCII character: " + quote(c.toString)) else char_symbols(c.toInt) } def is_ascii(s: Symbol): Boolean = s.length == 1 && s(0) < 128 /* symbol matching */ private val symbol_total = new Regex("""(?xs) [\ud800-\udbff][\udc00-\udfff] | \r\n | \\ < \^? ([A-Za-z][A-Za-z0-9_']*)? >? | .""") private def is_plain(c: Char): Boolean = !(c == '\r' || c == '\\' || Character.isHighSurrogate(c)) def is_malformed(s: Symbol): Boolean = s.length match { case 1 => val c = s(0) Character.isHighSurrogate(c) || Character.isLowSurrogate(c) || c == '\ufffd' case 2 => val c1 = s(0) val c2 = s(1) !(c1 == '\r' && c2 == '\n' || Character.isSurrogatePair(c1, c2)) case _ => !s.endsWith(">") || s == "\\<>" || s == "\\<^>" } def is_newline(s: Symbol): Boolean = s == "\n" || s == "\r" || s == "\r\n" class Matcher(text: CharSequence) { private val matcher = symbol_total.pattern.matcher(text) def apply(start: Int, end: Int): Int = { require(0 <= start && start < end && end <= text.length) if (is_plain(text.charAt(start))) 1 else { matcher.region(start, end).lookingAt matcher.group.length } } } /* iterator */ private val char_symbols: Array[Symbol] = (0 until 256).iterator.map(i => new String(Array(i.toChar))).toArray def iterator(text: CharSequence): Iterator[Symbol] = new Iterator[Symbol] { private val matcher = new Matcher(text) private var i = 0 def hasNext = i < text.length def next = { val n = matcher(i, text.length) val s = if (n == 0) "" else if (n == 1) { val c = text.charAt(i) if (c < char_symbols.length) char_symbols(c) else text.subSequence(i, i + n).toString } else text.subSequence(i, i + n).toString i += n s } } def explode(text: CharSequence): List[Symbol] = iterator(text).toList def length(text: CharSequence): Int = iterator(text).length def trim_blanks(text: CharSequence): String = Library.trim(is_blank(_), explode(text)).mkString def all_blank(str: String): Boolean = iterator(str).forall(is_blank(_)) def trim_blank_lines(text: String): String = cat_lines(split_lines(text).dropWhile(all_blank).reverse.dropWhile(all_blank).reverse) /* decoding offsets */ object Index { private sealed case class Entry(chr: Int, sym: Int) val empty: Index = new Index(Nil) def apply(text: CharSequence): Index = { val matcher = new Matcher(text) val buf = new mutable.ListBuffer[Entry] var chr = 0 var sym = 0 while (chr < text.length) { val n = matcher(chr, text.length) chr += n sym += 1 if (n > 1) buf += Entry(chr, sym) } if (buf.isEmpty) empty else new Index(buf.toList) } } final class Index private(entries: List[Index.Entry]) { private val hash: Int = entries.hashCode private val index: Array[Index.Entry] = entries.toArray def decode(symbol_offset: Offset): Text.Offset = { val sym = symbol_offset - 1 val end = index.length @tailrec def bisect(a: Int, b: Int): Int = { if (a < b) { val c = (a + b) / 2 if (sym < index(c).sym) bisect(a, c) else if (c + 1 == end || sym < index(c + 1).sym) c else bisect(c + 1, b) } else -1 } val i = bisect(0, end) if (i < 0) sym else index(i).chr + sym - index(i).sym } def decode(symbol_range: Range): Text.Range = symbol_range.map(decode(_)) override def hashCode: Int = hash override def equals(that: Any): Boolean = that match { case other: Index => index.sameElements(other.index) case _ => false } } /* symbolic text chunks -- without actual text */ object Text_Chunk { sealed abstract class Name case object Default extends Name case class Id(id: Document_ID.Generic) extends Name case class File(name: String) extends Name val encode_name: XML.Encode.T[Name] = { import XML.Encode._ variant(List( { case Default => (Nil, Nil) }, { case Id(a) => (List(long_atom(a)), Nil) }, { case File(a) => (List(a), Nil) })) } val decode_name: XML.Decode.T[Name] = { import XML.Decode._ variant(List( { case (Nil, Nil) => Default }, { case (List(a), Nil) => Id(long_atom(a)) }, { case (List(a), Nil) => File(a) })) } def apply(text: CharSequence): Text_Chunk = new Text_Chunk(Text.Range(0, text.length), Index(text)) } final class Text_Chunk private(val range: Text.Range, private val index: Index) { override def hashCode: Int = (range, index).hashCode override def equals(that: Any): Boolean = that match { case other: Text_Chunk => range == other.range && index == other.index case _ => false } override def toString: String = "Text_Chunk" + range.toString def decode(symbol_offset: Offset): Text.Offset = index.decode(symbol_offset) def decode(symbol_range: Range): Text.Range = index.decode(symbol_range) def incorporate(symbol_range: Range): Option[Text.Range] = { def in(r: Range): Option[Text.Range] = range.try_restrict(decode(r)) match { case Some(r1) if !r1.is_singularity => Some(r1) case _ => None } in(symbol_range) orElse in(symbol_range - 1) } } /* recoding text */ private class Recoder(list: List[(String, String)]) { private val (min, max) = { var min = '\uffff' var max = '\u0000' for ((x, _) <- list) { val c = x(0) if (c < min) min = c if (c > max) max = c } (min, max) } private val table = { var tab = Map[String, String]() for ((x, y) <- list) { tab.get(x) match { case None => tab += (x -> y) case Some(z) => error("Duplicate symbol mapping of " + quote(x) + " to " + quote(y) + " vs. " + quote(z)) } } tab } def recode(text: String): String = { val len = text.length val matcher = symbol_total.pattern.matcher(text) val result = new StringBuilder(len) var i = 0 while (i < len) { val c = text(i) if (min <= c && c <= max) { matcher.region(i, len).lookingAt val x = matcher.group result.append(table.getOrElse(x, x)) i = matcher.end } else { result.append(c); i += 1 } } result.toString } } /** symbol interpretation **/ val ARGUMENT_CARTOUCHE = "cartouche" val ARGUMENT_SPACE_CARTOUCHE = "space_cartouche" private lazy val symbols = { val contents = for (path <- Path.split(Isabelle_System.getenv("ISABELLE_SYMBOLS")) if path.is_file) yield (File.read(path)) new Interpretation(cat_lines(contents)) } private class Interpretation(symbols_spec: String) { /* read symbols */ private val No_Decl = new Regex("""(?xs) ^\s* (?: \#.* )? $ """) private val Key = new Regex("""(?xs) (.+): """) private def read_decl(decl: String): (Symbol, Properties.T) = { def err() = error("Bad symbol declaration: " + decl) def read_props(props: List[String]): Properties.T = { props match { case Nil => Nil case _ :: Nil => err() case Key(x) :: y :: rest => (x -> y.replace('\u2423', ' ')) :: read_props(rest) case _ => err() } } decl.split("\\s+").toList match { case sym :: props if sym.length > 1 && !is_malformed(sym) => (sym, read_props(props)) case _ => err() } } private val symbols: List[(Symbol, Properties.T)] = (((List.empty[(Symbol, Properties.T)], Set.empty[Symbol]) /: split_lines(symbols_spec).reverse) { case (res, No_Decl()) => res case ((list, known), decl) => val (sym, props) = read_decl(decl) if (known(sym)) (list, known) else ((sym, props) :: list, known + sym) })._1 /* basic properties */ val properties: Map[Symbol, Properties.T] = Map(symbols: _*) val names: Map[Symbol, (String, String)] = { val Name = new Regex("""\\<\^?([A-Za-z][A-Za-z0-9_']*)>""") val Argument = new Properties.String("argument") def argument(sym: Symbol, props: Properties.T): String = props match { case Argument(arg) => if (arg == ARGUMENT_CARTOUCHE || arg == ARGUMENT_SPACE_CARTOUCHE) arg else error("Bad argument: " + quote(arg) + " for symbol " + quote(sym)) case _ => "" } Map((for ((sym @ Name(a), props) <- symbols) yield sym -> (a, argument(sym, props))): _*) } val groups: List[(String, List[Symbol])] = symbols.map({ case (sym, props) => val gs = for (("group", g) <- props) yield g if (gs.isEmpty) List(sym -> "unsorted") else gs.map(sym -> _) }).flatten .groupBy(_._2).toList.map({ case (group, list) => (group, list.map(_._1)) }) .sortBy(_._1) val abbrevs: Multi_Map[Symbol, String] = Multi_Map(( for { (sym, props) <- symbols ("abbrev", a) <- props.reverse } yield sym -> a): _*) val codes: List[(Symbol, Int)] = { val Code = new Properties.String("code") for { (sym, props) <- symbols code <- props match { case Code(s) => try { Some(Integer.decode(s).intValue) } catch { case _: NumberFormatException => error("Bad code for symbol " + sym) } case _ => None } } yield { if (code < 128) error("Illegal ASCII code for symbol " + sym) else (sym, code) } } /* recoding */ private val (decoder, encoder) = { val mapping = for ((sym, code) <- codes) yield (sym, new String(Character.toChars(code))) (new Recoder(mapping), new Recoder(for ((x, y) <- mapping) yield (y, x))) } def decode(text: String): String = decoder.recode(text) def encode(text: String): String = encoder.recode(text) private def recode_set(elems: String*): Set[String] = { val content = elems.toList Set((content ::: content.map(decode)): _*) } private def recode_map[A](elems: (String, A)*): Map[String, A] = { val content = elems.toList Map((content ::: content.map({ case (sym, a) => (decode(sym), a) })): _*) } /* user fonts */ private val Font = new Properties.String("font") val fonts: Map[Symbol, String] = recode_map((for ((sym, Font(font)) <- symbols) yield sym -> font): _*) val font_names: List[String] = Set(fonts.toList.map(_._2): _*).toList val font_index: Map[String, Int] = Map((font_names zip (0 until font_names.length).toList): _*) /* classification */ val letters = recode_set( "A", "B", "C", "D", "E", "F", "G", "H", "I", "J", "K", "L", "M", "N", "O", "P", "Q", "R", "S", "T", "U", "V", "W", "X", "Y", "Z", "a", "b", "c", "d", "e", "f", "g", "h", "i", "j", "k", "l", "m", "n", "o", "p", "q", "r", "s", "t", "u", "v", "w", "x", "y", "z", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\

", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\

", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\

", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\
", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\") val blanks = recode_set(space, "\t", "\n", "\u000B", "\f", "\r", "\r\n") val sym_chars = Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~") val symbolic = recode_set((for { (sym, _) <- symbols; if raw_symbolic(sym) } yield sym): _*) /* misc symbols */ val newline_decoded = decode(newline) - val marker_decoded = decode(marker) val comment_decoded = decode(comment) val cancel_decoded = decode(cancel) val latex_decoded = decode(latex) + val marker_decoded = decode(marker) val open_decoded = decode(open) val close_decoded = decode(close) /* control symbols */ val control_decoded: Set[Symbol] = Set((for ((sym, _) <- symbols if sym.startsWith("\\<^")) yield decode(sym)): _*) val sub_decoded = decode(sub) val sup_decoded = decode(sup) val bold_decoded = decode(bold) val emph_decoded = decode(emph) val bsub_decoded = decode(bsub) val esub_decoded = decode(esub) val bsup_decoded = decode(bsup) val esup_decoded = decode(esup) } /* tables */ def properties: Map[Symbol, Properties.T] = symbols.properties def names: Map[Symbol, (String, String)] = symbols.names def groups: List[(String, List[Symbol])] = symbols.groups def abbrevs: Multi_Map[Symbol, String] = symbols.abbrevs def codes: List[(Symbol, Int)] = symbols.codes def groups_code: List[(String, List[Symbol])] = { val has_code = codes.iterator.map(_._1).toSet groups.flatMap({ case (group, symbols) => val symbols1 = symbols.filter(has_code) if (symbols1.isEmpty) None else Some((group, symbols1)) }) } lazy val is_code: Int => Boolean = codes.map(_._2).toSet def decode(text: String): String = symbols.decode(text) def encode(text: String): String = symbols.encode(text) def decode_yxml(text: String): XML.Body = YXML.parse_body(decode(text)) def decode_yxml_failsafe(text: String): XML.Body = YXML.parse_body_failsafe(decode(text)) def encode_yxml(body: XML.Body): String = encode(YXML.string_of_body(body)) def decode_strict(text: String): String = { val decoded = decode(text) if (encode(decoded) == text) decoded else { val bad = new mutable.ListBuffer[Symbol] for (s <- iterator(text) if encode(decode(s)) != s && !bad.contains(s)) bad += s error("Bad Unicode symbols in text: " + commas_quote(bad)) } } def fonts: Map[Symbol, String] = symbols.fonts def font_names: List[String] = symbols.font_names def font_index: Map[String, Int] = symbols.font_index def lookup_font(sym: Symbol): Option[Int] = symbols.fonts.get(sym).map(font_index(_)) /* classification */ def is_letter(sym: Symbol): Boolean = symbols.letters.contains(sym) def is_digit(sym: Symbol): Boolean = sym.length == 1 && '0' <= sym(0) && sym(0) <= '9' def is_quasi(sym: Symbol): Boolean = sym == "_" || sym == "'" 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) /* symbolic newline */ val newline: Symbol = "\\" def newline_decoded: Symbol = symbols.newline_decoded def print_newlines(str: String): String = if (str.contains('\n')) (for (s <- iterator(str)) yield { if (s == "\n") newline_decoded else s }).mkString else str - /* marker */ - - val marker: Symbol = "\\" - def marker_decoded: Symbol = symbols.marker_decoded - - lazy val is_marker: Set[Symbol] = Set(marker, marker_decoded) - - /* formal comments */ val comment: Symbol = "\\" val cancel: Symbol = "\\<^cancel>" val latex: Symbol = "\\<^latex>" + val marker: Symbol = "\\<^marker>" def comment_decoded: Symbol = symbols.comment_decoded def cancel_decoded: Symbol = symbols.cancel_decoded def latex_decoded: Symbol = symbols.latex_decoded + def marker_decoded: Symbol = symbols.marker_decoded /* cartouches */ val open: Symbol = "\\" val close: Symbol = "\\" 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 def cartouche(s: String): String = open + s + close def cartouche_decoded(s: String): String = open_decoded + s + close_decoded /* 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 */ val control_prefix = "\\<^" val control_suffix = ">" def control_name(sym: Symbol): Option[String] = if (is_control_encoded(sym)) Some(sym.substring(control_prefix.length, sym.length - control_suffix.length)) else None def is_control_encoded(sym: Symbol): Boolean = sym.startsWith(control_prefix) && sym.endsWith(control_suffix) def is_control(sym: Symbol): Boolean = 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) && !is_malformed(sym) && sym != "\"" val sub = "\\<^sub>" val sup = "\\<^sup>" val bold = "\\<^bold>" val emph = "\\<^emph>" val bsub = "\\<^bsub>" val esub = "\\<^esub>" val bsup = "\\<^bsup>" val esup = "\\<^esup>" def sub_decoded: Symbol = symbols.sub_decoded def sup_decoded: Symbol = symbols.sup_decoded def bold_decoded: Symbol = symbols.bold_decoded def emph_decoded: Symbol = symbols.emph_decoded def bsub_decoded: Symbol = symbols.bsub_decoded def esub_decoded: Symbol = symbols.esub_decoded def bsup_decoded: Symbol = symbols.bsup_decoded def esup_decoded: Symbol = symbols.esup_decoded } diff --git a/src/Pure/Isar/outer_syntax.ML b/src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML +++ b/src/Pure/Isar/outer_syntax.ML @@ -1,317 +1,332 @@ (* Title: Pure/Isar/outer_syntax.ML Author: Markus Wenzel, TU Muenchen Isabelle/Isar outer syntax. *) signature OUTER_SYNTAX = sig val help: theory -> string list -> unit val print_commands: theory -> unit type command_keyword = string * Position.T val command: command_keyword -> string -> (Toplevel.transition -> Toplevel.transition) parser -> unit val maybe_begin_local_theory: command_keyword -> string -> (local_theory -> local_theory) parser -> (theory -> local_theory) parser -> unit val local_theory': command_keyword -> string -> (bool -> local_theory -> local_theory) parser -> unit val local_theory: command_keyword -> string -> (local_theory -> local_theory) parser -> unit val local_theory_to_proof': command_keyword -> string -> (bool -> local_theory -> Proof.state) parser -> unit val local_theory_to_proof: command_keyword -> string -> (local_theory -> Proof.state) parser -> unit val bootstrap: bool Config.T - val parse_tokens: theory -> Token.T list -> Toplevel.transition list - val parse: theory -> Position.T -> string -> Toplevel.transition list val parse_spans: Token.T list -> Command_Span.span list val make_span: Token.T list -> Command_Span.span + val parse_span: theory -> (unit -> theory) -> Token.T list -> Toplevel.transition + val parse_text: theory -> (unit -> theory) -> Position.T -> string -> Toplevel.transition list val command_reports: theory -> Token.T -> Position.report_text list val check_command: Proof.context -> command_keyword -> string end; structure Outer_Syntax: OUTER_SYNTAX = struct (** outer syntax **) (* errors *) fun err_command msg name ps = error (msg ^ quote (Markup.markup Markup.keyword1 name) ^ Position.here_list ps); fun err_dup_command name ps = err_command "Duplicate outer syntax command " name ps; (* command parsers *) datatype command_parser = Parser of (Toplevel.transition -> Toplevel.transition) parser | Restricted_Parser of (bool * Position.T) option -> (Toplevel.transition -> Toplevel.transition) parser; datatype command = Command of {comment: string, command_parser: command_parser, pos: Position.T, id: serial}; fun eq_command (Command {id = id1, ...}, Command {id = id2, ...}) = id1 = id2; fun new_command comment command_parser pos = Command {comment = comment, command_parser = command_parser, pos = pos, id = serial ()}; fun command_pos (Command {pos, ...}) = pos; fun command_markup def (name, Command {pos, id, ...}) = Markup.properties (Position.entity_properties_of def id pos) (Markup.entity Markup.commandN name); fun pretty_command (cmd as (name, Command {comment, ...})) = Pretty.block (Pretty.marks_str ([Active.make_markup Markup.sendbackN {implicit = true, properties = [Markup.padding_line]}, command_markup false cmd], name) :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment); (* theory data *) structure Data = Theory_Data ( type T = command Symtab.table; val empty = Symtab.empty; val extend = I; fun merge data : T = data |> Symtab.join (fn name => fn (cmd1, cmd2) => if eq_command (cmd1, cmd2) then raise Symtab.SAME else err_dup_command name [command_pos cmd1, command_pos cmd2]); ); val get_commands = Data.get; val dest_commands = get_commands #> Symtab.dest #> sort_by #1; val lookup_commands = Symtab.lookup o get_commands; fun help thy pats = dest_commands thy |> filter (fn (name, _) => forall (fn pat => match_string pat name) pats) |> map pretty_command |> Pretty.writeln_chunks; fun print_commands thy = let val keywords = Thy_Header.get_keywords thy; val minor = Scan.dest_lexicon (Keyword.minor_keywords keywords); val commands = dest_commands thy; in [Pretty.strs ("keywords:" :: map quote minor), Pretty.big_list "commands:" (map pretty_command commands)] |> Pretty.writeln_chunks end; (* maintain commands *) fun add_command name cmd thy = if member (op =) Thy_Header.bootstrap_thys (Context.theory_name thy) then thy else let val _ = Keyword.is_command (Thy_Header.get_keywords thy) name orelse err_command "Undeclared outer syntax command " name [command_pos cmd]; val _ = (case lookup_commands thy name of NONE => () | SOME cmd' => err_dup_command name [command_pos cmd, command_pos cmd']); val _ = Context_Position.report_generic (Context.the_generic_context ()) (command_pos cmd) (command_markup true (name, cmd)); in Data.map (Symtab.update (name, cmd)) thy end; val _ = Theory.setup (Theory.at_end (fn thy => let val command_keywords = Scan.dest_lexicon (Keyword.major_keywords (Thy_Header.get_keywords thy)); val _ = (case subtract (op =) (map #1 (dest_commands thy)) command_keywords of [] => () | missing => error ("Missing outer syntax command(s) " ^ commas_quote missing)) in NONE end)); (* implicit theory setup *) type command_keyword = string * Position.T; fun raw_command (name, pos) comment command_parser = let val setup = add_command name (new_command comment command_parser pos) in Context.>> (Context.mapping setup (Local_Theory.background_theory setup)) end; fun command (name, pos) comment parse = raw_command (name, pos) comment (Parser parse); fun maybe_begin_local_theory command_keyword comment parse_local parse_global = raw_command command_keyword comment (Restricted_Parser (fn restricted => Parse.opt_target -- parse_local >> (fn (target, f) => Toplevel.local_theory restricted target f) || (if is_some restricted then Scan.fail else parse_global >> Toplevel.begin_local_theory true))); fun local_theory_command trans command_keyword comment parse = raw_command command_keyword comment (Restricted_Parser (fn restricted => Parse.opt_target -- parse >> (fn (target, f) => trans restricted target f))); val local_theory' = local_theory_command Toplevel.local_theory'; val local_theory = local_theory_command Toplevel.local_theory; val local_theory_to_proof' = local_theory_command Toplevel.local_theory_to_proof'; val local_theory_to_proof = local_theory_command Toplevel.local_theory_to_proof; (** toplevel parsing **) -(* parse commands *) - -val bootstrap = Config.declare_bool ("Outer_Syntax.bootstrap", \<^here>) (K true); - -local - -val before_command = - Scan.option (Parse.position (Parse.private >> K true || Parse.qualified >> K false)); - -fun parse_command thy = - Scan.ahead (before_command |-- Parse.position Parse.command) :|-- (fn (name, pos) => - let - val keywords = Thy_Header.get_keywords thy; - val tr0 = - Toplevel.empty - |> Toplevel.name name - |> Toplevel.position pos - |> Keyword.is_proof_open keywords name ? Toplevel.skip_proof_open - |> Keyword.is_proof_close keywords name ? Toplevel.skip_proof_close; - val command_marker = - Parse.command |-- Document_Source.annotation >> (fn markers => Toplevel.markers markers tr0); - in - (case lookup_commands thy name of - SOME (Command {command_parser = Parser parse, ...}) => - Parse.!!! (command_marker -- parse) >> (op |>) - | SOME (Command {command_parser = Restricted_Parser parse, ...}) => - before_command :|-- (fn restricted => - Parse.!!! (command_marker -- parse restricted)) >> (op |>) - | NONE => - Scan.fail_with (fn _ => fn _ => - let - val msg = - if Config.get_global thy bootstrap - then "missing theory context for command " - else "undefined command "; - in msg ^ quote (Markup.markup Markup.keyword1 name) end)) - end); - -in - -fun parse_tokens thy = - filter Token.is_proper - #> Source.of_list - #> Source.source Token.stopper (Scan.bulk (fn xs => Parse.!!! (parse_command thy) xs)) - #> Source.exhaust; - -fun parse thy pos text = - Symbol_Pos.explode (text, pos) - |> Token.tokenize (Thy_Header.get_keywords thy) {strict = false} - |> parse_tokens thy; - -end; - - (* parse spans *) local fun ship span = let val kind = if forall Token.is_ignored span then Command_Span.Ignored_Span else if exists Token.is_error span then Command_Span.Malformed_Span else (case find_first Token.is_command span of NONE => Command_Span.Malformed_Span | SOME cmd => Command_Span.Command_Span (Token.content_of cmd, Token.pos_of cmd)); in cons (Command_Span.Span (kind, span)) end; fun flush (result, content, ignored) = result |> not (null content) ? ship (rev content) |> not (null ignored) ? ship (rev ignored); fun parse tok (result, content, ignored) = if Token.is_ignored tok then (result, content, tok :: ignored) else if Token.is_command_modifier tok orelse Token.is_command tok andalso (not (exists Token.is_command_modifier content) orelse exists Token.is_command content) then (flush (result, content, ignored), [tok], []) else (result, tok :: (ignored @ content), []); in fun parse_spans toks = fold parse toks ([], [], []) |> flush |> rev; end; fun make_span toks = (case parse_spans toks of [span] => span | _ => Command_Span.Span (Command_Span.Malformed_Span, toks)); +(* parse commands *) + +val bootstrap = Config.declare_bool ("Outer_Syntax.bootstrap", \<^here>) (K true); + +local + +val before_command = + Scan.option (Parse.position (Parse.private >> K true || Parse.qualified >> K false)); + +fun parse_command thy markers = + Scan.ahead (before_command |-- Parse.position Parse.command) :|-- (fn (name, pos) => + let + val keywords = Thy_Header.get_keywords thy; + val tr0 = + Toplevel.empty + |> Toplevel.name name + |> Toplevel.position pos + |> Keyword.is_proof_open keywords name ? Toplevel.skip_proof_open + |> Keyword.is_proof_close keywords name ? Toplevel.skip_proof_close; + val command_markers = + Parse.command |-- Document_Source.tags >> + (fn tags => Toplevel.markers (map Document_Marker.legacy_tag tags @ markers) tr0); + in + (case lookup_commands thy name of + SOME (Command {command_parser = Parser parse, ...}) => + Parse.!!! (command_markers -- parse) >> (op |>) + | SOME (Command {command_parser = Restricted_Parser parse, ...}) => + before_command :|-- (fn restricted => + Parse.!!! (command_markers -- parse restricted)) >> (op |>) + | NONE => + Scan.fail_with (fn _ => fn _ => + let + val msg = + if Config.get_global thy bootstrap + then "missing theory context for command " + else "undefined command "; + in msg ^ quote (Markup.markup Markup.keyword1 name) end)) + end); + +in + +fun parse_span thy init span = + let + val range = Token.range_of span; + val core_range = Token.core_range_of span; + + val markers = map Token.input_of (filter Token.is_document_marker span); + fun parse () = + filter Token.is_proper span + |> Source.of_list + |> Source.source Token.stopper (Scan.bulk (fn xs => Parse.!!! (parse_command thy markers) xs)) + |> Source.exhaust; + in + (case parse () of + [tr] => Toplevel.modify_init init tr + | [] => Toplevel.ignored (#1 range) + | _ => Toplevel.malformed (#1 core_range) "Exactly one command expected") + handle ERROR msg => Toplevel.malformed (#1 core_range) msg + end; + +fun parse_text thy init pos text = + Symbol_Pos.explode (text, pos) + |> Token.tokenize (Thy_Header.get_keywords thy) {strict = false} + |> parse_spans + |> map (Command_Span.content #> parse_span thy init); + +end; + + (* check commands *) fun command_reports thy tok = if Token.is_command tok then let val name = Token.content_of tok in (case lookup_commands thy name of NONE => [] | SOME cmd => [((Token.pos_of tok, command_markup false (name, cmd)), "")]) end else []; fun check_command ctxt (name, pos) = let val thy = Proof_Context.theory_of ctxt; val keywords = Thy_Header.get_keywords thy; in if Keyword.is_command keywords name then let val markup = Token.explode0 keywords name |> maps (command_reports thy) |> map (#2 o #1); val _ = Context_Position.reports ctxt (map (pair pos) markup); in name end else let val completion_report = Completion.make_report (name, pos) (fn completed => Keyword.dest_commands keywords |> filter completed |> sort_strings |> map (fn a => (a, (Markup.commandN, a)))); in error ("Bad command " ^ quote name ^ Position.here pos ^ completion_report) end end; (* 'ML' command -- required for bootstrapping Isar *) val _ = command ("ML", \<^here>) "ML text within theory or local theory" (Parse.ML_source >> (fn source => Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source) #> Local_Theory.propagate_ml_env))); end; diff --git a/src/Pure/Isar/parse.ML b/src/Pure/Isar/parse.ML --- a/src/Pure/Isar/parse.ML +++ b/src/Pure/Isar/parse.ML @@ -1,487 +1,492 @@ (* Title: Pure/Isar/parse.ML Author: Markus Wenzel, TU Muenchen Generic parsers for Isabelle/Isar outer syntax. *) signature PARSE = sig val group: (unit -> string) -> (Token.T list -> 'a) -> Token.T list -> 'a val !!! : (Token.T list -> 'a) -> Token.T list -> 'a val !!!! : (Token.T list -> 'a) -> Token.T list -> 'a val not_eof: Token.T parser val token: 'a parser -> Token.T parser val range: 'a parser -> ('a * Position.range) parser val position: 'a parser -> ('a * Position.T) parser val input: 'a parser -> Input.source parser val inner_syntax: 'a parser -> string parser val command: string parser val keyword: string parser val short_ident: string parser val long_ident: string parser val sym_ident: string parser val dots: string parser val minus: string parser val term_var: string parser val type_ident: string parser val type_var: string parser val number: string parser val float_number: string parser val string: string parser val string_position: (string * Position.T) parser val alt_string: string parser val verbatim: string parser val cartouche: string parser val eof: string parser val command_name: string -> string parser val keyword_with: (string -> bool) -> string parser val keyword_markup: bool * Markup.T -> string -> string parser val keyword_improper: string -> string parser val $$$ : string -> string parser val reserved: string -> string parser val underscore: string parser val maybe: 'a parser -> 'a option parser val maybe_position: ('a * Position.T) parser -> ('a option * Position.T) parser val opt_keyword: string -> bool parser val opt_bang: bool parser val begin: string parser val opt_begin: bool parser val nat: int parser val int: int parser val real: real parser val enum_positions: string -> 'a parser -> ('a list * Position.T list) parser val enum1_positions: string -> 'a parser -> ('a list * Position.T list) parser val enum: string -> 'a parser -> 'a list parser val enum1: string -> 'a parser -> 'a list parser val and_list: 'a parser -> 'a list parser val and_list1: 'a parser -> 'a list parser val enum': string -> 'a context_parser -> 'a list context_parser val enum1': string -> 'a context_parser -> 'a list context_parser val and_list': 'a context_parser -> 'a list context_parser val and_list1': 'a context_parser -> 'a list context_parser val list: 'a parser -> 'a list parser val list1: 'a parser -> 'a list parser val properties: Properties.T parser val name: string parser val name_range: (string * Position.range) parser val name_position: (string * Position.T) parser val binding: binding parser val embedded: string parser val embedded_position: (string * Position.T) parser val text: string parser val path: string parser val session_name: (string * Position.T) parser val theory_name: (string * Position.T) parser val liberal_name: string parser val parname: string parser val parbinding: binding parser val class: string parser val sort: string parser val type_const: string parser val arity: (string * string list * string) parser val multi_arity: (string list * string list * string) parser val type_args: string list parser val type_args_constrained: (string * string option) list parser val typ: string parser val mixfix: mixfix parser val mixfix': mixfix parser val opt_mixfix: mixfix parser val opt_mixfix': mixfix parser val syntax_mode: Syntax.mode parser val where_: string parser val const_decl: (string * string * mixfix) parser val const_binding: (binding * string * mixfix) parser val params: (binding * string option * mixfix) list parser val vars: (binding * string option * mixfix) list parser val for_fixes: (binding * string option * mixfix) list parser val ML_source: Input.source parser val document_source: Input.source parser + val document_marker: Input.source parser val const: string parser val term: string parser val prop: string parser val literal_fact: string parser val propp: (string * string list) parser val termp: (string * string list) parser val private: Position.T parser val qualified: Position.T parser val target: (string * Position.T) parser val opt_target: (string * Position.T) option parser val args: Token.T list parser val args1: (string -> bool) -> Token.T list parser val attribs: Token.src list parser val opt_attribs: Token.src list parser val thm_sel: Facts.interval list parser val thm: (Facts.ref * Token.src list) parser val thms1: (Facts.ref * Token.src list) list parser val options: ((string * Position.T) * (string * Position.T)) list parser end; structure Parse: PARSE = struct (** error handling **) (* group atomic parsers (no cuts!) *) fun group s scan = scan || Scan.fail_with (fn [] => (fn () => s () ^ " expected,\nbut end-of-input was found") | tok :: _ => (fn () => (case Token.text_of tok of (txt, "") => s () ^ " expected,\nbut " ^ txt ^ Position.here (Token.pos_of tok) ^ " was found" | (txt1, txt2) => s () ^ " expected,\nbut " ^ txt1 ^ Position.here (Token.pos_of tok) ^ " was found:\n" ^ txt2))); (* cut *) fun cut kind scan = let fun get_pos [] = " (end-of-input)" | get_pos (tok :: _) = Position.here (Token.pos_of tok); fun err (toks, NONE) = (fn () => kind ^ get_pos toks) | err (toks, SOME msg) = (fn () => let val s = msg () in if String.isPrefix kind s then s else kind ^ get_pos toks ^ ": " ^ s end); in Scan.!! err scan end; fun !!! scan = cut "Outer syntax error" scan; fun !!!! scan = cut "Corrupted outer syntax in presentation" scan; (** basic parsers **) (* tokens *) fun RESET_VALUE atom = (*required for all primitive parsers*) Scan.ahead (Scan.one (K true)) -- atom >> (fn (arg, x) => (Token.assign NONE arg; x)); val not_eof = RESET_VALUE (Scan.one Token.not_eof); fun token atom = Scan.ahead not_eof --| atom; fun range scan = (Scan.ahead not_eof >> (Token.range_of o single)) -- scan >> Library.swap; fun position scan = (Scan.ahead not_eof >> Token.pos_of) -- scan >> Library.swap; fun input atom = Scan.ahead atom |-- not_eof >> Token.input_of; fun inner_syntax atom = Scan.ahead atom |-- not_eof >> Token.inner_syntax_of; fun kind k = group (fn () => Token.str_of_kind k) (RESET_VALUE (Scan.one (Token.is_kind k) >> Token.content_of)); val command = kind Token.Command; val keyword = kind Token.Keyword; val short_ident = kind Token.Ident; val long_ident = kind Token.Long_Ident; val sym_ident = kind Token.Sym_Ident; val term_var = kind Token.Var; val type_ident = kind Token.Type_Ident; val type_var = kind Token.Type_Var; val number = kind Token.Nat; val float_number = kind Token.Float; val string = kind Token.String; val alt_string = kind Token.Alt_String; val verbatim = kind Token.Verbatim; val cartouche = kind Token.Cartouche; val eof = kind Token.EOF; fun command_name x = group (fn () => Token.str_of_kind Token.Command ^ " " ^ quote x) (RESET_VALUE (Scan.one (fn tok => Token.is_command tok andalso Token.content_of tok = x))) >> Token.content_of; fun keyword_with pred = RESET_VALUE (Scan.one (Token.keyword_with pred) >> Token.content_of); fun keyword_markup markup x = group (fn () => Token.str_of_kind Token.Keyword ^ " " ^ quote x) (Scan.ahead not_eof -- keyword_with (fn y => x = y)) >> (fn (tok, x) => (Token.assign (SOME (Token.Literal markup)) tok; x)); val keyword_improper = keyword_markup (true, Markup.improper); val $$$ = keyword_markup (false, Markup.quasi_keyword); fun reserved x = group (fn () => "reserved identifier " ^ quote x) (RESET_VALUE (Scan.one (Token.ident_with (fn y => x = y)) >> Token.content_of)); val dots = sym_ident :-- (fn "\" => Scan.succeed () | _ => Scan.fail) >> #1; val minus = sym_ident :-- (fn "-" => Scan.succeed () | _ => Scan.fail) >> #1; val underscore = sym_ident :-- (fn "_" => Scan.succeed () | _ => Scan.fail) >> #1; fun maybe scan = underscore >> K NONE || scan >> SOME; fun maybe_position scan = position (underscore >> K NONE) || scan >> apfst SOME; val nat = number >> (#1 o Library.read_int o Symbol.explode); val int = Scan.optional (minus >> K ~1) 1 -- nat >> op *; val real = float_number >> Value.parse_real || int >> Real.fromInt; fun opt_keyword s = Scan.optional ($$$ "(" |-- !!! (($$$ s >> K true) --| $$$ ")")) false; val opt_bang = Scan.optional ($$$ "!" >> K true) false; val begin = $$$ "begin"; val opt_begin = Scan.optional (begin >> K true) false; (* enumerations *) fun enum1_positions sep scan = scan -- Scan.repeat (position ($$$ sep) -- !!! scan) >> (fn (x, ys) => (x :: map #2 ys, map (#2 o #1) ys)); fun enum_positions sep scan = enum1_positions sep scan || Scan.succeed ([], []); fun enum1 sep scan = scan ::: Scan.repeat ($$$ sep |-- !!! scan); fun enum sep scan = enum1 sep scan || Scan.succeed []; fun enum1' sep scan = scan ::: Scan.repeat (Scan.lift ($$$ sep) |-- scan); fun enum' sep scan = enum1' sep scan || Scan.succeed []; fun and_list1 scan = enum1 "and" scan; fun and_list scan = enum "and" scan; fun and_list1' scan = enum1' "and" scan; fun and_list' scan = enum' "and" scan; fun list1 scan = enum1 "," scan; fun list scan = enum "," scan; val properties = $$$ "(" |-- !!! (list (string -- ($$$ "=" |-- string)) --| $$$ ")"); (* names and embedded content *) val name = group (fn () => "name") (short_ident || long_ident || sym_ident || number || string); val name_range = input name >> Input.source_content_range; val name_position = input name >> Input.source_content; val string_position = input string >> Input.source_content; val binding = name_position >> Binding.make; val embedded = group (fn () => "embedded content") (cartouche || string || short_ident || long_ident || sym_ident || term_var || type_ident || type_var || number); val embedded_position = input embedded >> Input.source_content; val text = group (fn () => "text") (embedded || verbatim); val path = group (fn () => "file name/path specification") embedded; val session_name = group (fn () => "session name") name_position; val theory_name = group (fn () => "theory name") name_position; val liberal_name = keyword_with Token.ident_or_symbolic || name; val parname = Scan.optional ($$$ "(" |-- name --| $$$ ")") ""; val parbinding = Scan.optional ($$$ "(" |-- binding --| $$$ ")") Binding.empty; (* type classes *) val class = group (fn () => "type class") (inner_syntax embedded); val sort = group (fn () => "sort") (inner_syntax embedded); val type_const = group (fn () => "type constructor") (inner_syntax embedded); val arity = type_const -- ($$$ "::" |-- !!! (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> Scan.triple2; val multi_arity = and_list1 type_const -- ($$$ "::" |-- !!! (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> Scan.triple2; (* types *) val typ = group (fn () => "type") (inner_syntax embedded); fun type_arguments arg = arg >> single || $$$ "(" |-- !!! (list1 arg --| $$$ ")") || Scan.succeed []; val type_args = type_arguments type_ident; val type_args_constrained = type_arguments (type_ident -- Scan.option ($$$ "::" |-- !!! sort)); (* mixfix annotations *) local val mfix = input (string || cartouche); val mixfix_ = mfix -- !!! (Scan.optional ($$$ "[" |-- !!! (list nat --| $$$ "]")) [] -- Scan.optional nat 1000) >> (fn (sy, (ps, p)) => fn range => Mixfix (sy, ps, p, range)); val structure_ = $$$ "structure" >> K Structure; val binder_ = $$$ "binder" |-- !!! (mfix -- ($$$ "[" |-- nat --| $$$ "]" -- nat || nat >> (fn n => (n, n)))) >> (fn (sy, (p, q)) => fn range => Binder (sy, p, q, range)); val infixl_ = $$$ "infixl" |-- !!! (mfix -- nat >> (fn (sy, p) => fn range => Infixl (sy, p, range))); val infixr_ = $$$ "infixr" |-- !!! (mfix -- nat >> (fn (sy, p) => fn range => Infixr (sy, p, range))); val infix_ = $$$ "infix" |-- !!! (mfix -- nat >> (fn (sy, p) => fn range => Infix (sy, p, range))); val mixfix_body = mixfix_ || structure_ || binder_ || infixl_ || infixr_ || infix_; fun annotation guard body = Scan.trace ($$$ "(" |-- guard (body --| $$$ ")")) >> (fn (mx, toks) => mx (Token.range_of toks)); fun opt_annotation guard body = Scan.optional (annotation guard body) NoSyn; in val mixfix = annotation !!! mixfix_body; val mixfix' = annotation I mixfix_body; val opt_mixfix = opt_annotation !!! mixfix_body; val opt_mixfix' = opt_annotation I mixfix_body; end; (* syntax mode *) val syntax_mode_spec = ($$$ "output" >> K ("", false)) || name -- Scan.optional ($$$ "output" >> K false) true; val syntax_mode = Scan.optional ($$$ "(" |-- !!! (syntax_mode_spec --| $$$ ")")) Syntax.mode_default; (* fixes *) val where_ = $$$ "where"; val const_decl = name -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> Scan.triple1; val const_binding = binding -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> Scan.triple1; val param_mixfix = binding -- Scan.option ($$$ "::" |-- typ) -- mixfix' >> (single o Scan.triple1); val params = (binding -- Scan.repeat binding) -- Scan.option ($$$ "::" |-- !!! (Scan.ahead typ -- embedded)) >> (fn ((x, ys), T) => (x, Option.map #1 T, NoSyn) :: map (fn y => (y, Option.map #2 T, NoSyn)) ys); val vars = and_list1 (param_mixfix || params) >> flat; val for_fixes = Scan.optional ($$$ "for" |-- !!! vars) []; (* embedded source text *) val ML_source = input (group (fn () => "ML source") text); val document_source = input (group (fn () => "document source") text); +val document_marker = + group (fn () => "document marker") + (RESET_VALUE (Scan.one Token.is_document_marker >> Token.input_of)); + (* terms *) val const = group (fn () => "constant") (inner_syntax embedded); val term = group (fn () => "term") (inner_syntax embedded); val prop = group (fn () => "proposition") (inner_syntax embedded); val literal_fact = inner_syntax (group (fn () => "literal fact") (alt_string || cartouche)); (* patterns *) val is_terms = Scan.repeat1 ($$$ "is" |-- term); val is_props = Scan.repeat1 ($$$ "is" |-- prop); val propp = prop -- Scan.optional ($$$ "(" |-- !!! (is_props --| $$$ ")")) []; val termp = term -- Scan.optional ($$$ "(" |-- !!! (is_terms --| $$$ ")")) []; (* target information *) val private = position ($$$ "private") >> #2; val qualified = position ($$$ "qualified") >> #2; val target = ($$$ "(" -- $$$ "in") |-- !!! (name_position --| $$$ ")"); val opt_target = Scan.option target; (* arguments within outer syntax *) local val argument_kinds = [Token.Ident, Token.Long_Ident, Token.Sym_Ident, Token.Var, Token.Type_Ident, Token.Type_Var, Token.Nat, Token.Float, Token.String, Token.Alt_String, Token.Cartouche, Token.Verbatim]; fun arguments is_symid = let fun argument blk = group (fn () => "argument") (Scan.one (fn tok => let val kind = Token.kind_of tok in member (op =) argument_kinds kind orelse Token.keyword_with is_symid tok orelse (blk andalso Token.keyword_with (fn s => s = ",") tok) end)); fun args blk x = Scan.optional (args1 blk) [] x and args1 blk x = (Scan.repeats1 (Scan.repeat1 (argument blk) || argsp "(" ")" || argsp "[" "]")) x and argsp l r x = (token ($$$ l) ::: !!! (args true @@@ (token ($$$ r) >> single))) x; in (args, args1) end; in val args = #1 (arguments Token.ident_or_symbolic) false; fun args1 is_symid = #2 (arguments is_symid) false; end; (* attributes *) val attrib = token liberal_name ::: !!! args; val attribs = $$$ "[" |-- list attrib --| $$$ "]"; val opt_attribs = Scan.optional attribs []; (* theorem references *) val thm_sel = $$$ "(" |-- list1 (nat --| minus -- nat >> Facts.FromTo || nat --| minus >> Facts.From || nat >> Facts.Single) --| $$$ ")"; val thm = $$$ "[" |-- attribs --| $$$ "]" >> pair (Facts.named "") || (literal_fact >> Facts.Fact || name_position -- Scan.option thm_sel >> Facts.Named) -- opt_attribs; val thms1 = Scan.repeat1 thm; (* options *) val option_name = group (fn () => "option name") name_position; val option_value = group (fn () => "option value") ((token real || token name) >> Token.content_of); val option = option_name :-- (fn (_, pos) => Scan.optional ($$$ "=" |-- !!! (position option_value)) ("true", pos)); val options = $$$ "[" |-- list1 option --| $$$ "]"; end; diff --git a/src/Pure/Isar/parse.scala b/src/Pure/Isar/parse.scala --- a/src/Pure/Isar/parse.scala +++ b/src/Pure/Isar/parse.scala @@ -1,105 +1,104 @@ /* Title: Pure/Isar/parse.scala Author: Makarius Generic parsers for Isabelle/Isar outer syntax. */ package isabelle import scala.util.parsing.combinator.Parsers import scala.annotation.tailrec object Parse { /* parsing tokens */ trait Parser extends Parsers { type Elem = Token def filter_proper: Boolean = true @tailrec private def proper(in: Input): Input = if (!filter_proper || in.atEnd || in.first.is_proper) in else proper(in.rest) private def proper_position: Parser[Position.T] = new Parser[Position.T] { def apply(raw_input: Input) = { val in = proper(raw_input) val pos = in.pos match { case pos: Token.Pos => pos case _ => Token.Pos.none } Success(if (in.atEnd) pos.position() else pos.position(in.first), in) } } def position[A](parser: Parser[A]): Parser[(A, Position.T)] = proper_position ~ parser ^^ { case x ~ y => (y, x) } def token(s: String, pred: Elem => Boolean): Parser[Elem] = new Parser[Elem] { def apply(raw_input: Input) = { val in = proper(raw_input) if (in.atEnd) Failure(s + " expected,\nbut end-of-input was found", in) else { val token = in.first if (pred(token)) Success(token, proper(in.rest)) else Failure(s + " expected,\nbut " + token.kind + " was found:\n" + token.source, in) } } } def atom(s: String, pred: Elem => Boolean): Parser[String] = token(s, pred) ^^ (_.content) def command(name: String): Parser[String] = atom("command " + quote(name), _.is_command(name)) def $$$(name: String): Parser[String] = atom("keyword " + quote(name), _.is_keyword(name)) def string: Parser[String] = atom("string", _.is_string) def nat: Parser[Int] = atom("natural number", _.is_nat) ^^ (s => Integer.parseInt(s)) def name: Parser[String] = atom("name", _.is_name) def embedded: Parser[String] = atom("embedded content", _.is_embedded) def text: Parser[String] = atom("text", _.is_text) def ML_source: Parser[String] = atom("ML source", _.is_text) def document_source: Parser[String] = atom("document source", _.is_text) def path: Parser[String] = atom("file name/path specification", tok => tok.is_embedded && Path.is_wellformed(tok.content)) def session_name: Parser[String] = atom("session name", _.is_system_name) def theory_name: Parser[String] = atom("theory name", _.is_system_name) private def tag_name: Parser[String] = atom("tag name", tok => tok.kind == Token.Kind.IDENT || tok.kind == Token.Kind.STRING) def tag: Parser[String] = $$$("%") ~> tag_name def tags: Parser[List[String]] = rep(tag) - def marker: Parser[String] = - ($$$(Symbol.marker) | $$$(Symbol.marker_decoded)) ~! embedded ^^ { case _ ~ x => x } + def marker: Parser[String] = token("marker", _.is_marker) ^^ (_.content) - def annotation: Parser[Unit] = rep(marker | tag) ^^ { case _ => () } + def annotation: Parser[Unit] = rep(tag | marker) ^^ { case _ => () } /* wrappers */ def parse[T](p: Parser[T], in: Token.Reader): ParseResult[T] = p(in) def parse_all[T](p: Parser[T], in: Token.Reader): ParseResult[T] = { val result = parse(p, in) val rest = proper(result.next) if (result.successful && !rest.atEnd) Error("bad input", rest) else result } } } diff --git a/src/Pure/Isar/token.ML b/src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML +++ b/src/Pure/Isar/token.ML @@ -1,787 +1,798 @@ (* Title: Pure/Isar/token.ML Author: Markus Wenzel, TU Muenchen Outer token syntax for Isabelle/Isar. *) signature TOKEN = sig datatype kind = (*immediate source*) Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat | Float | Space | (*delimited content*) String | Alt_String | Verbatim | Cartouche | Comment of Comment.kind option | (*special content*) Error of string | EOF val str_of_kind: kind -> string type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T} type T type src = T list type name_value = {name: string, kind: string, print: Proof.context -> Markup.T * xstring} datatype value = Source of src | Literal of bool * Markup.T | Name of name_value * morphism | Typ of typ | Term of term | Fact of string option * thm list | Attribute of morphism -> attribute | Declaration of declaration | Files of file Exn.result list val pos_of: T -> Position.T - val range_of: T list -> Position.range val adjust_offsets: (int -> int option) -> T -> T val eof: T val is_eof: T -> bool val not_eof: T -> bool val stopper: T Scan.stopper val kind_of: T -> kind val is_kind: kind -> T -> bool val is_command: T -> bool val keyword_with: (string -> bool) -> T -> bool val is_command_modifier: T -> bool val ident_with: (string -> bool) -> T -> bool val is_proper: T -> bool val is_comment: T -> bool val is_informal_comment: T -> bool val is_formal_comment: T -> bool + val is_document_marker: T -> bool val is_ignored: T -> bool val is_begin_ignore: T -> bool val is_end_ignore: T -> bool val is_error: T -> bool val is_space: T -> bool val is_blank: T -> bool val is_newline: T -> bool + val range_of: T list -> Position.range + val core_range_of: T list -> Position.range val content_of: T -> string val source_of: T -> string val input_of: T -> Input.source val inner_syntax_of: T -> string val keyword_markup: bool * Markup.T -> string -> Markup.T val completion_report: T -> Position.report_text list val reports: Keyword.keywords -> T -> Position.report_text list val markups: Keyword.keywords -> T -> Markup.T list val unparse: T -> string val print: T -> string val text_of: T -> string * string val file_source: file -> Input.source val get_files: T -> file Exn.result list val put_files: file Exn.result list -> T -> T val get_value: T -> value option val reports_of_value: T -> Position.report list val name_value: name_value -> value val get_name: T -> name_value option val declare_maxidx: T -> Proof.context -> Proof.context val map_facts: (string option -> thm list -> thm list) -> T -> T val trim_context_src: src -> src val transform: morphism -> T -> T val init_assignable: T -> T val assign: value option -> T -> T val evaluate: ('a -> value) -> (T -> 'a) -> T -> 'a val closure: T -> T val pretty_value: Proof.context -> T -> Pretty.T val name_of_src: src -> string * Position.T val args_of_src: src -> T list val checked_src: src -> bool val check_src: Proof.context -> (Proof.context -> 'a Name_Space.table) -> src -> src * 'a val pretty_src: Proof.context -> src -> Pretty.T val ident_or_symbolic: string -> bool val read_cartouche: Symbol_Pos.T list -> T val tokenize: Keyword.keywords -> {strict: bool} -> Symbol_Pos.T list -> T list val explode: Keyword.keywords -> Position.T -> string -> T list val explode0: Keyword.keywords -> string -> T list val print_name: Keyword.keywords -> string -> string val make: (int * int) * string -> Position.T -> T * Position.T val make_string: string * Position.T -> T val make_int: int -> T list val make_src: string * Position.T -> T list -> src type 'a parser = T list -> 'a * T list type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list) val read_body: Keyword.keywords -> 'a parser -> Symbol_Pos.T list -> 'a option val read_antiq: Keyword.keywords -> 'a parser -> Symbol_Pos.T list * Position.T -> 'a val syntax_generic: 'a context_parser -> src -> Context.generic -> 'a * Context.generic val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context end; structure Token: TOKEN = struct (** tokens **) (* token kind *) datatype kind = (*immediate source*) Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat | Float | Space | (*delimited content*) String | Alt_String | Verbatim | Cartouche | Comment of Comment.kind option | (*special content*) Error of string | EOF; val str_of_kind = fn Command => "command" | Keyword => "keyword" | Ident => "identifier" | Long_Ident => "long identifier" | Sym_Ident => "symbolic identifier" | Var => "schematic variable" | Type_Ident => "type variable" | Type_Var => "schematic type variable" | Nat => "natural number" | Float => "floating-point number" | Space => "white space" | String => "quoted string" | Alt_String => "back-quoted string" | Verbatim => "verbatim text" | Cartouche => "text cartouche" | Comment NONE => "informal comment" | Comment (SOME _) => "formal comment" | Error _ => "bad input" | EOF => "end-of-input"; val immediate_kinds = Vector.fromList [Command, Keyword, Ident, Long_Ident, Sym_Ident, Var, Type_Ident, Type_Var, Nat, Float, Space]; val delimited_kind = (fn String => true | Alt_String => true | Verbatim => true | Cartouche => true | Comment _ => true | _ => false); (* datatype token *) (*The value slot assigns an (optional) internal value to a token, usually as a side-effect of special scanner setup (see also args.ML). Note that an assignable ref designates an intermediate state of internalization -- it is NOT meant to persist.*) type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T}; type name_value = {name: string, kind: string, print: Proof.context -> Markup.T * xstring}; datatype T = Token of (Symbol_Pos.text * Position.range) * (kind * string) * slot and slot = Slot | Value of value option | Assignable of value option Unsynchronized.ref and value = Source of T list | Literal of bool * Markup.T | Name of name_value * morphism | Typ of typ | Term of term | Fact of string option * thm list | (*optional name for dynamic fact, i.e. fact "variable"*) Attribute of morphism -> attribute | Declaration of declaration | Files of file Exn.result list; type src = T list; (* position *) fun pos_of (Token ((_, (pos, _)), _, _)) = pos; fun end_pos_of (Token ((_, (_, pos)), _, _)) = pos; -fun range_of (toks as tok :: _) = - let val pos' = end_pos_of (List.last toks) - in Position.range (pos_of tok, pos') end - | range_of [] = Position.no_range; - fun adjust_offsets adjust (Token ((x, range), y, z)) = Token ((x, apply2 (Position.adjust_offsets adjust) range), y, z); (* stopper *) fun mk_eof pos = Token (("", (pos, Position.none)), (EOF, ""), Slot); val eof = mk_eof Position.none; fun is_eof (Token (_, (EOF, _), _)) = true | is_eof _ = false; val not_eof = not o is_eof; val stopper = Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof; (* kind of token *) fun kind_of (Token (_, (k, _), _)) = k; fun is_kind k (Token (_, (k', _), _)) = k = k'; val is_command = is_kind Command; fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x | keyword_with _ _ = false; val is_command_modifier = keyword_with (fn x => x = "private" orelse x = "qualified"); fun ident_with pred (Token (_, (Ident, x), _)) = pred x | ident_with _ _ = false; fun is_ignored (Token (_, (Space, _), _)) = true | is_ignored (Token (_, (Comment NONE, _), _)) = true | is_ignored _ = false; fun is_proper (Token (_, (Space, _), _)) = false | is_proper (Token (_, (Comment _, _), _)) = false | is_proper _ = true; fun is_comment (Token (_, (Comment _, _), _)) = true | is_comment _ = false; fun is_informal_comment (Token (_, (Comment NONE, _), _)) = true | is_informal_comment _ = false; fun is_formal_comment (Token (_, (Comment (SOME _), _), _)) = true | is_formal_comment _ = false; +fun is_document_marker (Token (_, (Comment (SOME Comment.Marker), _), _)) = true + | is_document_marker _ = false; + fun is_begin_ignore (Token (_, (Comment NONE, "<"), _)) = true | is_begin_ignore _ = false; fun is_end_ignore (Token (_, (Comment NONE, ">"), _)) = true | is_end_ignore _ = false; fun is_error (Token (_, (Error _, _), _)) = true | is_error _ = false; (* blanks and newlines -- space tokens obey lines *) fun is_space (Token (_, (Space, _), _)) = true | is_space _ = false; fun is_blank (Token (_, (Space, x), _)) = not (String.isSuffix "\n" x) | is_blank _ = false; fun is_newline (Token (_, (Space, x), _)) = String.isSuffix "\n" x | is_newline _ = false; +(* range of tokens *) + +fun range_of (toks as tok :: _) = + let val pos' = end_pos_of (List.last toks) + in Position.range (pos_of tok, pos') end + | range_of [] = Position.no_range; + +val core_range_of = + drop_prefix is_ignored #> drop_suffix is_ignored #> range_of; + + (* token content *) fun content_of (Token (_, (_, x), _)) = x; fun source_of (Token ((source, _), _, _)) = source; fun input_of (Token ((source, range), (kind, _), _)) = Input.source (delimited_kind kind) source range; fun inner_syntax_of tok = let val x = content_of tok in if YXML.detect x then x else Syntax.implode_input (input_of tok) end; (* markup reports *) local val token_kind_markup = fn Var => (Markup.var, "") | Type_Ident => (Markup.tfree, "") | Type_Var => (Markup.tvar, "") | String => (Markup.string, "") | Alt_String => (Markup.alt_string, "") | Verbatim => (Markup.verbatim, "") | Cartouche => (Markup.cartouche, "") | Comment _ => (Markup.comment, "") | Error msg => (Markup.bad (), msg) | _ => (Markup.empty, ""); fun keyword_reports tok = map (fn markup => ((pos_of tok, markup), "")); fun command_markups keywords x = if Keyword.is_theory_end keywords x then [Markup.keyword2 |> Markup.keyword_properties] else (if Keyword.is_proof_asm keywords x then [Markup.keyword3] else if Keyword.is_improper keywords x then [Markup.keyword1, Markup.improper] else [Markup.keyword1]) |> map Markup.command_properties; in fun keyword_markup (important, keyword) x = if important orelse Symbol.is_ascii_identifier x then keyword else Markup.delimiter; fun completion_report tok = if is_kind Keyword tok then map (fn m => ((pos_of tok, m), "")) (Completion.suppress_abbrevs (content_of tok)) else []; fun reports keywords tok = if is_command tok then keyword_reports tok (command_markups keywords (content_of tok)) else if is_kind Keyword tok then keyword_reports tok [keyword_markup (false, Markup.keyword2 |> Markup.keyword_properties) (content_of tok)] else let val pos = pos_of tok; val (m, text) = token_kind_markup (kind_of tok); val delete = #2 (Symbol_Pos.explode_delete (source_of tok, pos)); in ((pos, m), text) :: map (fn p => ((p, Markup.delete), "")) delete end; fun markups keywords = map (#2 o #1) o reports keywords; end; (* unparse *) fun unparse (Token (_, (kind, x), _)) = (case kind of String => Symbol_Pos.quote_string_qq x | Alt_String => Symbol_Pos.quote_string_bq x | Verbatim => enclose "{*" "*}" x | Cartouche => cartouche x | Comment NONE => enclose "(*" "*)" x | EOF => "" | _ => x); fun print tok = Markup.markups (markups Keyword.empty_keywords tok) (unparse tok); fun text_of tok = let val k = str_of_kind (kind_of tok); val ms = markups Keyword.empty_keywords tok; val s = unparse tok; in if s = "" then (k, "") else if size s < 40 andalso not (exists_string (fn c => c = "\n") s) then (k ^ " " ^ Markup.markups ms s, "") else (k, Markup.markups ms s) end; (** associated values **) (* inlined file content *) fun file_source (file: file) = let val text = cat_lines (#lines file); val end_pos = fold Position.advance (Symbol.explode text) (#pos file); in Input.source true text (Position.range (#pos file, end_pos)) end; fun get_files (Token (_, _, Value (SOME (Files files)))) = files | get_files _ = []; fun put_files [] tok = tok | put_files files (Token (x, y, Slot)) = Token (x, y, Value (SOME (Files files))) | put_files _ tok = raise Fail ("Cannot put inlined files here" ^ Position.here (pos_of tok)); (* access values *) fun get_value (Token (_, _, Value v)) = v | get_value _ = NONE; fun map_value f (Token (x, y, Value (SOME v))) = Token (x, y, Value (SOME (f v))) | map_value _ tok = tok; (* reports of value *) fun get_assignable_value (Token (_, _, Assignable r)) = ! r | get_assignable_value (Token (_, _, Value v)) = v | get_assignable_value _ = NONE; fun reports_of_value tok = (case get_assignable_value tok of SOME (Literal markup) => let val pos = pos_of tok; val x = content_of tok; in if Position.is_reported pos then map (pair pos) (keyword_markup markup x :: Completion.suppress_abbrevs x) else [] end | _ => []); (* name value *) fun name_value a = Name (a, Morphism.identity); fun get_name tok = (case get_assignable_value tok of SOME (Name (a, _)) => SOME a | _ => NONE); (* maxidx *) fun declare_maxidx tok = (case get_value tok of SOME (Source src) => fold declare_maxidx src | SOME (Typ T) => Variable.declare_maxidx (Term.maxidx_of_typ T) | SOME (Term t) => Variable.declare_maxidx (Term.maxidx_of_term t) | SOME (Fact (_, ths)) => fold (Variable.declare_maxidx o Thm.maxidx_of) ths | SOME (Attribute _) => I (* FIXME !? *) | SOME (Declaration decl) => (fn ctxt => let val ctxt' = Context.proof_map (Morphism.form decl) ctxt in Variable.declare_maxidx (Variable.maxidx_of ctxt') ctxt end) | _ => I); (* fact values *) fun map_facts f = map_value (fn v => (case v of Source src => Source (map (map_facts f) src) | Fact (a, ths) => Fact (a, f a ths) | _ => v)); val trim_context_src = (map o map_facts) (K (map Thm.trim_context)); (* transform *) fun transform phi = map_value (fn v => (case v of Source src => Source (map (transform phi) src) | Literal _ => v | Name (a, psi) => Name (a, psi $> phi) | Typ T => Typ (Morphism.typ phi T) | Term t => Term (Morphism.term phi t) | Fact (a, ths) => Fact (a, Morphism.fact phi ths) | Attribute att => Attribute (Morphism.transform phi att) | Declaration decl => Declaration (Morphism.transform phi decl) | Files _ => v)); (* static binding *) (*1st stage: initialize assignable slots*) fun init_assignable tok = (case tok of Token (x, y, Slot) => Token (x, y, Assignable (Unsynchronized.ref NONE)) | Token (_, _, Value _) => tok | Token (_, _, Assignable r) => (r := NONE; tok)); (*2nd stage: assign values as side-effect of scanning*) fun assign v tok = (case tok of Token (x, y, Slot) => Token (x, y, Value v) | Token (_, _, Value _) => tok | Token (_, _, Assignable r) => (r := v; tok)); fun evaluate mk eval arg = let val x = eval arg in (assign (SOME (mk x)) arg; x) end; (*3rd stage: static closure of final values*) fun closure (Token (x, y, Assignable (Unsynchronized.ref v))) = Token (x, y, Value v) | closure tok = tok; (* pretty *) fun pretty_value ctxt tok = (case get_value tok of SOME (Literal markup) => let val x = content_of tok in Pretty.mark_str (keyword_markup markup x, x) end | SOME (Name ({print, ...}, _)) => Pretty.quote (Pretty.mark_str (print ctxt)) | SOME (Typ T) => Syntax.pretty_typ ctxt T | SOME (Term t) => Syntax.pretty_term ctxt t | SOME (Fact (_, ths)) => Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.cartouche o Thm.pretty_thm ctxt) ths)) | _ => Pretty.marks_str (markups Keyword.empty_keywords tok, unparse tok)); (* src *) fun dest_src ([]: src) = raise Fail "Empty token source" | dest_src (head :: args) = (head, args); fun name_of_src src = let val head = #1 (dest_src src); val name = (case get_name head of SOME {name, ...} => name | NONE => content_of head); in (name, pos_of head) end; val args_of_src = #2 o dest_src; fun pretty_src ctxt src = let val (head, args) = dest_src src; val prt_name = (case get_name head of SOME {print, ...} => Pretty.mark_str (print ctxt) | NONE => Pretty.str (content_of head)); in Pretty.block (Pretty.breaks (Pretty.quote prt_name :: map (pretty_value ctxt) args)) end; fun checked_src (head :: _) = is_some (get_name head) | checked_src [] = true; fun check_src ctxt get_table src = let val (head, args) = dest_src src; val table = get_table ctxt; in (case get_name head of SOME {name, ...} => (src, Name_Space.get table name) | NONE => let val pos = pos_of head; val (name, x) = Name_Space.check (Context.Proof ctxt) table (content_of head, pos); val _ = Context_Position.report ctxt pos Markup.operator; val kind = Name_Space.kind_of (Name_Space.space_of_table table); fun print ctxt' = Name_Space.markup_extern ctxt' (Name_Space.space_of_table (get_table ctxt')) name; val value = name_value {name = name, kind = kind, print = print}; val head' = closure (assign (SOME value) head); in (head' :: args, x) end) end; (** scanners **) open Basic_Symbol_Pos; val err_prefix = "Outer lexical error: "; fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg); (* scan symbolic idents *) val scan_symid = 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 Symbol.is_symbolic_char s | SOME ss => forall Symbol.is_symbolic_char ss | _ => false); fun ident_or_symbolic "begin" = false | ident_or_symbolic ":" = true | ident_or_symbolic "::" = true | ident_or_symbolic s = Symbol_Pos.is_identifier s orelse is_symid s; (* scan verbatim text *) val scan_verb = $$$ "*" --| Scan.ahead (~$$ "}") || Scan.one (fn (s, _) => s <> "*" andalso Symbol.not_eof s) >> single; val scan_verbatim = Scan.ahead ($$ "{" -- $$ "*") |-- !!! "unclosed verbatim text" ((Symbol_Pos.scan_pos --| $$ "{" --| $$ "*") -- (Scan.repeats scan_verb -- ($$ "*" |-- $$ "}" |-- Symbol_Pos.scan_pos))); val recover_verbatim = $$$ "{" @@@ $$$ "*" @@@ Scan.repeats scan_verb; (* scan cartouche *) val scan_cartouche = Symbol_Pos.scan_pos -- ((Symbol_Pos.scan_cartouche err_prefix >> Symbol_Pos.cartouche_content) -- Symbol_Pos.scan_pos); (* scan space *) fun space_symbol (s, _) = Symbol.is_blank s andalso s <> "\n"; val scan_space = Scan.many1 space_symbol @@@ Scan.optional ($$$ "\n") [] || Scan.many space_symbol @@@ $$$ "\n"; (* scan comment *) val scan_comment = Symbol_Pos.scan_pos -- (Symbol_Pos.scan_comment_body err_prefix -- Symbol_Pos.scan_pos); (** token sources **) local fun token_leq ((_, syms1), (_, syms2)) = length syms1 <= length syms2; fun token k ss = Token ((Symbol_Pos.implode ss, Symbol_Pos.range ss), (k, Symbol_Pos.content ss), Slot); fun token_range k (pos1, (ss, pos2)) = Token (Symbol_Pos.implode_range (pos1, pos2) ss, (k, Symbol_Pos.content ss), Slot); fun scan_token keywords = !!! "bad input" (Symbol_Pos.scan_string_qq err_prefix >> token_range String || Symbol_Pos.scan_string_bq err_prefix >> token_range Alt_String || scan_verbatim >> token_range Verbatim || scan_cartouche >> token_range Cartouche || scan_comment >> token_range (Comment NONE) || - Comment.scan >> (fn (k, ss) => token (Comment (SOME k)) ss) || + Comment.scan_outer >> (fn (k, ss) => token (Comment (SOME k)) ss) || scan_space >> token Space || (Scan.max token_leq (Scan.max token_leq (Scan.literal (Keyword.major_keywords keywords) >> pair Command) (Scan.literal (Keyword.minor_keywords keywords) >> pair Keyword)) (Lexicon.scan_longid >> pair Long_Ident || Lexicon.scan_id >> pair Ident || Lexicon.scan_var >> pair Var || Lexicon.scan_tid >> pair Type_Ident || Lexicon.scan_tvar >> pair Type_Var || Symbol_Pos.scan_float >> pair Float || Symbol_Pos.scan_nat >> pair Nat || scan_symid >> pair Sym_Ident) >> uncurry token)); fun recover msg = (Symbol_Pos.recover_string_qq || Symbol_Pos.recover_string_bq || recover_verbatim || Symbol_Pos.recover_cartouche || Symbol_Pos.recover_comment || Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> single) >> (single o token (Error msg)); in fun make_source keywords {strict} = let val scan_strict = Scan.bulk (scan_token keywords); val scan = if strict then scan_strict else Scan.recover scan_strict recover; in Source.source Symbol_Pos.stopper scan end; fun read_cartouche syms = (case Scan.read Symbol_Pos.stopper (scan_cartouche >> token_range Cartouche) syms of SOME tok => tok | NONE => error ("Single cartouche expected" ^ Position.here (#1 (Symbol_Pos.range syms)))); end; (* explode *) fun tokenize keywords strict syms = Source.of_list syms |> make_source keywords strict |> Source.exhaust; fun explode keywords pos text = Symbol_Pos.explode (text, pos) |> tokenize keywords {strict = false}; fun explode0 keywords = explode keywords Position.none; (* print name in parsable form *) fun print_name keywords name = ((case explode keywords Position.none name of [tok] => not (member (op =) [Ident, Long_Ident, Sym_Ident, Nat] (kind_of tok)) | _ => true) ? Symbol_Pos.quote_string_qq) name; (* make *) fun make ((k, n), s) pos = let val pos' = Position.advance_offsets n pos; val range = Position.range (pos, pos'); val tok = if 0 <= k andalso k < Vector.length immediate_kinds then Token ((s, range), (Vector.sub (immediate_kinds, k), s), Slot) else (case explode Keyword.empty_keywords pos s of [tok] => tok | _ => Token ((s, range), (Error (err_prefix ^ "exactly one token expected"), s), Slot)) in (tok, pos') end; fun make_string (s, pos) = let val Token ((x, _), y, z) = #1 (make ((~1, 0), Symbol_Pos.quote_string_qq s) Position.none); val pos' = Position.no_range_position pos; in Token ((x, (pos', pos')), y, z) end; val make_int = explode Keyword.empty_keywords Position.none o signed_string_of_int; fun make_src a args = make_string a :: args; (** parsers **) type 'a parser = T list -> 'a * T list; type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list); (* read body -- e.g. antiquotation source *) fun read_body keywords scan = tokenize (Keyword.no_command_keywords keywords) {strict = true} #> filter is_proper #> Scan.read stopper scan; fun read_antiq keywords scan (syms, pos) = (case read_body keywords scan syms of SOME x => x | NONE => error ("Malformed antiquotation" ^ Position.here pos)); (* wrapped syntax *) fun syntax_generic scan src context = let val (name, pos) = name_of_src src; val old_reports = maps reports_of_value src; val args1 = map init_assignable (args_of_src src); fun reported_text () = if Context_Position.is_visible_generic context then let val new_reports = maps (reports_of_value o closure) args1 in if old_reports <> new_reports then map (fn (p, m) => Position.reported_text p m "") new_reports else [] end else []; in (case Scan.error (Scan.finite' stopper (Scan.option scan)) (context, args1) of (SOME x, (context', [])) => let val _ = Output.report (reported_text ()) in (x, context') end | (_, (context', args2)) => let val print_name = (case get_name (hd src) of NONE => quote name | SOME {kind, print, ...} => let val ctxt' = Context.proof_of context'; val (markup, xname) = print ctxt'; in plain_words kind ^ " " ^ quote (Markup.markup markup xname) end); val print_args = if null args2 then "" else ":\n " ^ space_implode " " (map print args2); in error ("Bad arguments for " ^ print_name ^ Position.here pos ^ print_args ^ Markup.markup_report (implode (reported_text ()))) end) end; fun syntax scan src = apsnd Context.the_proof o syntax_generic scan src o Context.Proof; end; type 'a parser = 'a Token.parser; type 'a context_parser = 'a Token.context_parser; diff --git a/src/Pure/Isar/token.scala b/src/Pure/Isar/token.scala --- a/src/Pure/Isar/token.scala +++ b/src/Pure/Isar/token.scala @@ -1,344 +1,347 @@ /* Title: Pure/Isar/token.scala Author: Makarius Outer token syntax for Isabelle/Isar. */ package isabelle import scala.collection.mutable import scala.util.parsing.input object Token { /* tokens */ object Kind extends Enumeration { /*immediate source*/ val COMMAND = Value("command") val KEYWORD = Value("keyword") val IDENT = Value("identifier") val LONG_IDENT = Value("long identifier") val SYM_IDENT = Value("symbolic identifier") val VAR = Value("schematic variable") val TYPE_IDENT = Value("type variable") val TYPE_VAR = Value("schematic type variable") val NAT = Value("natural number") val FLOAT = Value("floating-point number") val SPACE = Value("white space") /*delimited content*/ val STRING = Value("string") val ALT_STRING = Value("back-quoted string") val VERBATIM = Value("verbatim text") val CARTOUCHE = Value("text cartouche") val INFORMAL_COMMENT = Value("informal comment") val FORMAL_COMMENT = Value("formal comment") /*special content*/ val ERROR = Value("bad input") val UNPARSED = Value("unparsed input") } /* parsers */ object Parsers extends Parsers trait Parsers extends Scan.Parsers with Comment.Parsers { private def delimited_token: Parser[Token] = { 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.INFORMAL_COMMENT, x)) val formal_cmt = comment_cartouche ^^ (x => Token(Token.Kind.FORMAL_COMMENT, x)) string | (alt_string | (verb | (cart | (cmt | formal_cmt)))) } private def other_token(keywords: Keyword.Keywords): Parser[Token] = { val letdigs1 = many1(Symbol.is_letdig) val sub = one(s => s == Symbol.sub_decoded || s == Symbol.sub) val id = one(Symbol.is_letter) ~ (rep(letdigs1 | (sub ~ letdigs1 ^^ { case x ~ y => x + y })) ^^ (_.mkString)) ^^ { case x ~ y => x + y } val nat = many1(Symbol.is_digit) val natdot = nat ~ "." ~ nat ^^ { case x ~ y ~ z => x + y + z } val id_nat = id ~ opt("." ~ nat) ^^ { case x ~ Some(y ~ z) => x + y + z case x ~ None => x } val ident = id ~ rep("." ~> id) ^^ { case x ~ Nil => Token(Token.Kind.IDENT, x) case x ~ ys => Token(Token.Kind.LONG_IDENT, (x :: ys).mkString(".")) } val var_ = "?" ~ id_nat ^^ { case x ~ y => Token(Token.Kind.VAR, x + y) } val type_ident = "'" ~ id ^^ { case x ~ y => Token(Token.Kind.TYPE_IDENT, x + y) } val type_var = "?'" ~ id_nat ^^ { case x ~ y => Token(Token.Kind.TYPE_VAR, x + y) } val nat_ = nat ^^ (x => Token(Token.Kind.NAT, x)) val float = ("-" ~ natdot ^^ { case x ~ y => x + y } | natdot) ^^ (x => Token(Token.Kind.FLOAT, x)) val sym_ident = (many1(Symbol.is_symbolic_char) | one(sym => Symbol.is_symbolic(sym))) ^^ (x => Token(Token.Kind.SYM_IDENT, x)) val keyword = literal(keywords.minor) ^^ (x => Token(Token.Kind.KEYWORD, x)) ||| literal(keywords.major) ^^ (x => Token(Token.Kind.COMMAND, x)) val space = many1(Symbol.is_blank) ^^ (x => Token(Token.Kind.SPACE, x)) val recover_delimited = (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)) space | (recover_delimited | (((ident | (var_ | (type_ident | (type_var | (float | (nat_ | sym_ident)))))) ||| keyword) | bad)) } def token(keywords: Keyword.Keywords): Parser[Token] = delimited_token | other_token(keywords) def token_line(keywords: Keyword.Keywords, ctxt: Scan.Line_Context) : Parser[(Token, Scan.Line_Context)] = { val string = quoted_line("\"", ctxt) ^^ { case (x, c) => (Token(Token.Kind.STRING, x), c) } val alt_string = quoted_line("`", ctxt) ^^ { case (x, c) => (Token(Token.Kind.ALT_STRING, x), c) } val verb = verbatim_line(ctxt) ^^ { case (x, c) => (Token(Token.Kind.VERBATIM, x), c) } val cart = cartouche_line(ctxt) ^^ { case (x, c) => (Token(Token.Kind.CARTOUCHE, x), c) } val cmt = comment_line(ctxt) ^^ { case (x, c) => (Token(Token.Kind.INFORMAL_COMMENT, x), c) } val formal_cmt = comment_cartouche_line(ctxt) ^^ { case (x, c) => (Token(Token.Kind.FORMAL_COMMENT, x), c) } val other = other_token(keywords) ^^ { case x => (x, Scan.Finished) } string | (alt_string | (verb | (cart | (cmt | (formal_cmt | other))))) } } /* explode */ def explode(keywords: Keyword.Keywords, inp: CharSequence): List[Token] = Parsers.parseAll(Parsers.rep(Parsers.token(keywords)), Scan.char_reader(inp)) match { case Parsers.Success(tokens, _) => tokens case _ => error("Unexpected failure of tokenizing input:\n" + inp.toString) } def explode_line(keywords: Keyword.Keywords, inp: CharSequence, context: Scan.Line_Context) : (List[Token], Scan.Line_Context) = { var in: input.Reader[Char] = Scan.char_reader(inp) val toks = new mutable.ListBuffer[Token] var ctxt = context while (!in.atEnd) { Parsers.parse(Parsers.token_line(keywords, ctxt), in) match { case Parsers.Success((x, c), rest) => toks += x; ctxt = c; in = rest case Parsers.NoSuccess(_, rest) => error("Unexpected failure of tokenizing input:\n" + rest.source.toString) } } (toks.toList, ctxt) } val newline: Token = explode(Keyword.Keywords.empty, "\n").head /* embedded */ def read_embedded(keywords: Keyword.Keywords, inp: CharSequence): Option[Token] = explode(keywords, inp) match { case List(tok) if tok.is_embedded => Some(tok) case _ => None } /* names */ def read_name(keywords: Keyword.Keywords, inp: CharSequence): Option[Token] = explode(keywords, inp) match { case List(tok) if tok.is_name => Some(tok) case _ => None } def quote_name(keywords: Keyword.Keywords, name: String): String = if (read_name(keywords, name).isDefined) name 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 = toks match { case List(tok) => tok.source case _ => toks.map(_.source).mkString } /* token reader */ object Pos { val none: Pos = new Pos(0, 0, "", "") val start: Pos = new Pos(1, 1, "", "") def file(file: String): Pos = new Pos(1, 1, file, "") def id(id: String): Pos = new Pos(0, 1, "", id) val command: Pos = id(Markup.COMMAND) } final class Pos private[Token]( val line: Int, val offset: Symbol.Offset, val file: String, val id: String) extends input.Position { def column = 0 def lineContents = "" def advance(token: Token): Pos = advance(token.source) def advance(source: String): Pos = { var line1 = line var offset1 = offset for (s <- Symbol.iterator(source)) { if (line1 > 0 && Symbol.is_newline(s)) line1 += 1 if (offset1 > 0) offset1 += 1 } if (line1 == line && offset1 == offset) this else new Pos(line1, offset1, file, id) } private def position(end_offset: Symbol.Offset): Position.T = (if (line > 0) Position.Line(line) else Nil) ::: (if (offset > 0) Position.Offset(offset) else Nil) ::: (if (end_offset > 0) Position.End_Offset(end_offset) else Nil) ::: (if (file != "") Position.File(file) else Nil) ::: (if (id != "") Position.Id_String(id) else Nil) def position(): Position.T = position(0) def position(token: Token): Position.T = position(advance(token).offset) def position(source: String): Position.T = position(advance(source).offset) override def toString: String = Position.here(position(), delimited = false) } abstract class Reader extends input.Reader[Token] private class Token_Reader(tokens: List[Token], val pos: Pos) extends Reader { def first = tokens.head def rest = new Token_Reader(tokens.tail, pos.advance(first)) def atEnd = tokens.isEmpty } def reader(tokens: List[Token], start: Token.Pos): Reader = new Token_Reader(tokens, start) /* XML data representation */ val encode: XML.Encode.T[Token] = (tok: Token) => { import XML.Encode._ pair(int, string)(tok.kind.id, tok.source) } val decode: XML.Decode.T[Token] = (body: XML.Body) => { import XML.Decode._ val (k, s) = pair(int, string)(body) Token(Kind(k), s) } } sealed case class Token(kind: Token.Kind.Value, source: String) { def is_command: Boolean = kind == Token.Kind.COMMAND def is_command(name: String): Boolean = kind == Token.Kind.COMMAND && source == name def is_keyword: Boolean = kind == Token.Kind.KEYWORD def is_keyword(name: String): Boolean = kind == Token.Kind.KEYWORD && source == name def is_keyword(name: Char): Boolean = kind == Token.Kind.KEYWORD && source.length == 1 && source(0) == name def is_delimiter: Boolean = is_keyword && !Symbol.is_ascii_identifier(source) def is_ident: Boolean = kind == Token.Kind.IDENT def is_sym_ident: Boolean = kind == Token.Kind.SYM_IDENT def is_string: Boolean = kind == Token.Kind.STRING def is_nat: Boolean = kind == Token.Kind.NAT def is_float: Boolean = kind == Token.Kind.FLOAT def is_name: Boolean = kind == Token.Kind.IDENT || kind == Token.Kind.LONG_IDENT || kind == Token.Kind.SYM_IDENT || kind == Token.Kind.STRING || kind == Token.Kind.NAT def is_embedded: Boolean = is_name || kind == Token.Kind.CARTOUCHE || kind == Token.Kind.VAR || kind == Token.Kind.TYPE_IDENT || kind == Token.Kind.TYPE_VAR def is_text: Boolean = is_embedded || kind == Token.Kind.VERBATIM def is_space: Boolean = kind == Token.Kind.SPACE def is_informal_comment: Boolean = kind == Token.Kind.INFORMAL_COMMENT def is_formal_comment: Boolean = kind == Token.Kind.FORMAL_COMMENT + def is_marker: Boolean = + kind == Token.Kind.FORMAL_COMMENT && + (source.startsWith(Symbol.marker) || source.startsWith(Symbol.marker_decoded)) def is_comment: Boolean = is_informal_comment || is_formal_comment def is_ignored: Boolean = is_space || is_informal_comment def is_proper: Boolean = !is_space && !is_comment def is_error: Boolean = kind == Token.Kind.ERROR def is_unparsed: Boolean = kind == Token.Kind.UNPARSED def is_unfinished: Boolean = is_error && (source.startsWith("\"") || source.startsWith("`") || source.startsWith("{*") || source.startsWith("(*") || source.startsWith(Symbol.open) || source.startsWith(Symbol.open_decoded)) def is_open_bracket: Boolean = is_keyword && Word.open_brackets.exists(is_keyword(_)) def is_close_bracket: Boolean = is_keyword && Word.close_brackets.exists(is_keyword(_)) def is_begin: Boolean = is_keyword("begin") def is_end: Boolean = is_command("end") def is_begin_or_command: Boolean = is_begin || is_command def content: String = if (kind == Token.Kind.STRING) Scan.Parsers.quoted_content("\"", source) else if (kind == Token.Kind.ALT_STRING) Scan.Parsers.quoted_content("`", source) else if (kind == Token.Kind.VERBATIM) Scan.Parsers.verbatim_content(source) else if (kind == Token.Kind.CARTOUCHE) Scan.Parsers.cartouche_content(source) else if (kind == Token.Kind.INFORMAL_COMMENT) Scan.Parsers.comment_content(source) else if (kind == Token.Kind.FORMAL_COMMENT) Comment.content(source) else source def is_system_name: Boolean = { val s = content is_name && Path.is_wellformed(s) && !s.exists(Symbol.is_ascii_blank(_)) && !Path.is_reserved(s) } } diff --git a/src/Pure/ML/ml_lex.ML b/src/Pure/ML/ml_lex.ML --- a/src/Pure/ML/ml_lex.ML +++ b/src/Pure/ML/ml_lex.ML @@ -1,392 +1,392 @@ (* Title: Pure/ML/ml_lex.ML Author: Makarius Lexical syntax for Isabelle/ML and Standard ML. *) signature ML_LEX = sig val keywords: string list datatype token_kind = Keyword | Ident | Long_Ident | Type_Var | Word | Int | Real | Char | String | Space | Comment of Comment.kind option | Error of string | EOF eqtype token val stopper: token Scan.stopper val is_regular: token -> bool val is_improper: token -> bool val is_comment: token -> bool val set_range: Position.range -> token -> token val range_of: token -> Position.range val pos_of: token -> Position.T val end_pos_of: token -> Position.T val kind_of: token -> token_kind val content_of: token -> string val check_content_of: token -> string val flatten: token list -> string val source: (Symbol.symbol, 'a) Source.source -> (token, (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source val tokenize: string -> token list val read_text: Symbol_Pos.text * Position.T -> token Antiquote.antiquote list val read: Symbol_Pos.text -> token Antiquote.antiquote list val read_set_range: Position.range -> Symbol_Pos.text -> token Antiquote.antiquote list val read_source': {language: bool -> Markup.T, opaque_warning: bool, symbols: bool} -> token Antiquote.antiquote Symbol_Pos.scanner -> Input.source -> token Antiquote.antiquote list val read_source: Input.source -> token Antiquote.antiquote list val read_source_sml: Input.source -> token Antiquote.antiquote list val read_symbols_sml: Symbol_Pos.T list -> token Antiquote.antiquote list end; structure ML_Lex: ML_LEX = struct (** keywords **) val keywords = ["#", "(", ")", ",", "->", "...", ":", ":>", ";", "=", "=>", "[", "]", "_", "{", "|", "}", "abstype", "and", "andalso", "as", "case", "datatype", "do", "else", "end", "eqtype", "exception", "fn", "fun", "functor", "handle", "if", "in", "include", "infix", "infixr", "let", "local", "nonfix", "of", "op", "open", "orelse", "raise", "rec", "sharing", "sig", "signature", "struct", "structure", "then", "type", "val", "where", "while", "with", "withtype"]; val keywords2 = ["and", "case", "do", "else", "end", "if", "in", "let", "local", "of", "sig", "struct", "then", "while", "with"]; val keywords3 = ["handle", "open", "raise"]; val lexicon = Scan.make_lexicon (map raw_explode keywords); (** tokens **) (* datatype token *) datatype token_kind = Keyword | Ident | Long_Ident | Type_Var | Word | Int | Real | Char | String | Space | Comment of Comment.kind option | Error of string | EOF; datatype token = Token of Position.range * (token_kind * string); (* position *) fun set_range range (Token (_, x)) = Token (range, x); fun range_of (Token (range, _)) = range; val pos_of = #1 o range_of; val end_pos_of = #2 o range_of; (* stopper *) fun mk_eof pos = Token ((pos, Position.none), (EOF, "")); val eof = mk_eof Position.none; fun is_eof (Token (_, (EOF, _))) = true | is_eof _ = false; val stopper = Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof; (* token content *) fun kind_of (Token (_, (k, _))) = k; fun content_of (Token (_, (_, x))) = x; fun token_leq (tok, tok') = content_of tok <= content_of tok'; fun is_keyword (Token (_, (Keyword, _))) = true | is_keyword _ = false; fun is_delimiter (Token (_, (Keyword, x))) = not (Symbol.is_ascii_identifier x) | is_delimiter _ = false; fun is_regular (Token (_, (Error _, _))) = false | is_regular (Token (_, (EOF, _))) = false | is_regular _ = true; fun is_improper (Token (_, (Space, _))) = true | is_improper (Token (_, (Comment _, _))) = true | is_improper _ = false; fun is_comment (Token (_, (Comment _, _))) = true | is_comment _ = false; fun warning_opaque tok = (case tok of Token (_, (Keyword, ":>")) => warning ("Opaque signature matching (:>) fails to work with ML pretty printing --\n\ \prefer non-opaque matching (:) possibly with abstype" ^ Position.here (pos_of tok)) | _ => ()); fun check_content_of tok = (case kind_of tok of Error msg => error msg | _ => content_of tok); (* flatten *) fun flatten_content (tok :: (toks as tok' :: _)) = Symbol.escape (check_content_of tok) :: (if is_improper tok orelse is_improper tok' then flatten_content toks else Symbol.space :: flatten_content toks) | flatten_content toks = map (Symbol.escape o check_content_of) toks; val flatten = implode o flatten_content; (* markup *) local val token_kind_markup = fn Type_Var => (Markup.ML_tvar, "") | Word => (Markup.ML_numeral, "") | Int => (Markup.ML_numeral, "") | Real => (Markup.ML_numeral, "") | Char => (Markup.ML_char, "") | String => (Markup.ML_string, "") | Comment _ => (Markup.ML_comment, "") | Error msg => (Markup.bad (), msg) | _ => (Markup.empty, ""); in fun token_report (tok as Token ((pos, _), (kind, x))) = let val (markup, txt) = if not (is_keyword tok) then token_kind_markup kind else if is_delimiter tok then (Markup.ML_delimiter, "") else if member (op =) keywords2 x then (Markup.ML_keyword2 |> Markup.keyword_properties, "") else if member (op =) keywords3 x then (Markup.ML_keyword3 |> Markup.keyword_properties, "") else (Markup.ML_keyword1 |> Markup.keyword_properties, ""); in ((pos, markup), txt) end; end; (** scanners **) open Basic_Symbol_Pos; val err_prefix = "SML lexical error: "; fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg); (* identifiers *) local val scan_letdigs = Scan.many (Symbol.is_ascii_letdig o Symbol_Pos.symbol); val scan_alphanumeric = Scan.one (Symbol.is_ascii_letter o Symbol_Pos.symbol) ::: scan_letdigs; val scan_symbolic = Scan.many1 (member (op =) (raw_explode "!#$%&*+-/:<=>?@\\^`|~") o Symbol_Pos.symbol); in val scan_ident = scan_alphanumeric || scan_symbolic; val scan_long_ident = Scan.repeats1 (scan_alphanumeric @@@ $$$ ".") @@@ (scan_ident || $$$ "="); val scan_type_var = $$$ "'" @@@ scan_letdigs; end; (* numerals *) local val scan_dec = Scan.many1 (Symbol.is_ascii_digit o Symbol_Pos.symbol); val scan_hex = Scan.many1 (Symbol.is_ascii_hex o Symbol_Pos.symbol); val scan_sign = Scan.optional ($$$ "~") []; val scan_decint = scan_sign @@@ scan_dec; val scan_exp = ($$$ "E" || $$$ "e") @@@ scan_decint; in val scan_word = $$$ "0" @@@ $$$ "w" @@@ $$$ "x" @@@ scan_hex || $$$ "0" @@@ $$$ "w" @@@ scan_dec; val scan_int = scan_sign @@@ ($$$ "0" @@@ $$$ "x" @@@ scan_hex || scan_dec); val scan_rat = scan_decint @@@ Scan.optional ($$$ "/" @@@ scan_dec) []; val scan_real = scan_decint @@@ $$$ "." @@@ scan_dec @@@ Scan.optional scan_exp [] || scan_decint @@@ scan_exp; end; (* chars and strings *) val scan_blanks1 = Scan.many1 (Symbol.is_ascii_blank o Symbol_Pos.symbol); local val scan_escape = Scan.one (member (op =) (raw_explode "\"\\abtnvfr") o Symbol_Pos.symbol) >> single || $$$ "^" @@@ (Scan.one (fn (s, _) => Char.ord #"@" <= ord s andalso ord s <= Char.ord #"_") >> single) || Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) -- Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) -- Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) >> (fn ((a, b), c) => [a, b, c]); val scan_str = Scan.one (fn (s, _) => Symbol.not_eof s andalso s <> "\"" andalso s <> "\\" andalso (not (Symbol.is_char s) orelse Symbol.is_printable s)) >> single || $$$ "\\" @@@ !!! "bad escape character in string" scan_escape; val scan_gap = $$$ "\\" @@@ scan_blanks1 @@@ $$$ "\\"; val scan_gaps = Scan.repeats scan_gap; in val scan_char = $$$ "#" @@@ $$$ "\"" @@@ scan_gaps @@@ scan_str @@@ scan_gaps @@@ $$$ "\""; val recover_char = $$$ "#" @@@ $$$ "\"" @@@ scan_gaps @@@ Scan.optional (Scan.permissive scan_str @@@ scan_gaps) []; val scan_string = Scan.ahead ($$ "\"") |-- !!! "unclosed string literal" ($$$ "\"" @@@ Scan.repeats (scan_gap || scan_str) @@@ $$$ "\""); val recover_string = $$$ "\"" @@@ Scan.repeats (scan_gap || Scan.permissive scan_str); end; (* rat antiquotation *) val rat_name = Symbol_Pos.explode ("Pure.rat ", Position.none); val scan_rat_antiq = Symbol_Pos.scan_pos -- ($$ "@" |-- Symbol_Pos.scan_pos -- scan_rat) -- Symbol_Pos.scan_pos >> (fn ((pos1, (pos2, body)), pos3) => {start = Position.range_position (pos1, pos2), stop = Position.none, range = Position.range (pos1, pos3), body = rat_name @ body}); (* scan tokens *) local fun token k ss = Token (Symbol_Pos.range ss, (k, Symbol_Pos.content ss)); val scan_sml = scan_char >> token Char || scan_string >> token String || scan_blanks1 >> token Space || Symbol_Pos.scan_comment err_prefix >> token (Comment NONE) || Scan.max token_leq (Scan.literal lexicon >> token Keyword) (scan_word >> token Word || scan_real >> token Real || scan_int >> token Int || scan_long_ident >> token Long_Ident || scan_ident >> token Ident || scan_type_var >> token Type_Var); val scan_sml_antiq = scan_sml >> Antiquote.Text; val scan_ml_antiq = - Comment.scan >> (fn (kind, ss) => Antiquote.Text (token (Comment (SOME kind)) ss)) || + Comment.scan_inner >> (fn (kind, ss) => Antiquote.Text (token (Comment (SOME kind)) ss)) || Antiquote.scan_control >> Antiquote.Control || Antiquote.scan_antiq >> Antiquote.Antiq || scan_rat_antiq >> Antiquote.Antiq || scan_sml_antiq; fun recover msg = (recover_char || recover_string || Symbol_Pos.recover_cartouche || Symbol_Pos.recover_comment || Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> single) >> (single o token (Error msg)); fun reader {opaque_warning} scan syms = let val termination = if null syms then [] else let val pos1 = List.last syms |-> Position.advance; val pos2 = Position.advance Symbol.space pos1; in [Antiquote.Text (Token (Position.range (pos1, pos2), (Space, Symbol.space)))] end; fun check (Antiquote.Text tok) = (check_content_of tok; if opaque_warning then warning_opaque tok else ()) | check _ = (); val input = Source.of_list syms |> Source.source Symbol_Pos.stopper (Scan.recover (Scan.bulk (!!! "bad input" scan)) (fn msg => recover msg >> map Antiquote.Text)) |> Source.exhaust; val _ = Position.reports (Antiquote.antiq_reports input); val _ = Position.reports_text (maps (fn Antiquote.Text t => [token_report t] | _ => []) input); val _ = List.app check input; in input @ termination end; in fun source src = Symbol_Pos.source (Position.line 1) src |> Source.source Symbol_Pos.stopper (Scan.recover (Scan.bulk (!!! "bad input" scan_sml)) recover); val tokenize = Symbol.explode #> Source.of_list #> source #> Source.exhaust; val read_text = reader {opaque_warning = true} scan_ml_antiq o Symbol_Pos.explode; fun read text = read_text (text, Position.none); fun read_set_range range = read #> map (fn Antiquote.Text tok => Antiquote.Text (set_range range tok) | antiq => antiq); fun read_source' {language, symbols, opaque_warning} scan source = let val pos = Input.pos_of source; val _ = if Position.is_reported_range pos then Position.report pos (language (Input.is_delimited source)) else (); in Input.source_explode source |> not symbols ? maps (fn (s, p) => raw_explode s |> map (rpair p)) |> reader {opaque_warning = opaque_warning} scan end; val read_source = read_source' {language = Markup.language_ML, symbols = true, opaque_warning = true} scan_ml_antiq; val read_source_sml = read_source' {language = Markup.language_SML, symbols = false, opaque_warning = false} scan_sml_antiq; val read_symbols_sml = reader {opaque_warning = false} scan_sml_antiq; end; end; diff --git a/src/Pure/PIDE/command.ML b/src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML +++ b/src/Pure/PIDE/command.ML @@ -1,513 +1,508 @@ (* Title: Pure/PIDE/command.ML Author: Makarius Prover command execution: read -- eval -- print. *) signature COMMAND = sig type blob = (string * (SHA1.digest * string list) option) Exn.result val read_file: Path.T -> Position.T -> Path.T -> Token.file val read_thy: Toplevel.state -> theory val read: Keyword.keywords -> theory -> Path.T-> (unit -> theory) -> blob list * int -> Token.T list -> Toplevel.transition type eval val eval_command_id: eval -> Document_ID.command val eval_exec_id: eval -> Document_ID.exec val eval_eq: eval * eval -> bool val eval_running: eval -> bool val eval_finished: eval -> bool val eval_result_command: eval -> Toplevel.transition val eval_result_state: eval -> Toplevel.state val eval: Keyword.keywords -> Path.T -> (unit -> theory) -> blob list * int -> Document_ID.command -> Token.T list -> eval -> eval type print type print_fn = Toplevel.transition -> Toplevel.state -> unit val print0: {pri: int, print_fn: print_fn} -> eval -> print val print: bool -> (string * string list) list -> Keyword.keywords -> string -> eval -> print list -> print list option val parallel_print: print -> bool type print_function = {keywords: Keyword.keywords, command_name: string, args: string list, exec_id: Document_ID.exec} -> {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option val print_function: string -> print_function -> unit val no_print_function: string -> unit type exec = eval * print list val init_exec: theory option -> exec val no_exec: exec val exec_ids: exec option -> Document_ID.exec list val exec: Document_ID.execution -> exec -> unit val exec_parallel_prints: Document_ID.execution -> Future.task list -> exec -> exec option end; structure Command: COMMAND = struct (** main phases of execution **) fun task_context group f = f |> Future.interruptible_task |> Future.task_context "Command.run_process" group; (* read *) type blob = (string * (SHA1.digest * string list) option) Exn.result; (*file node name, digest, lines*) fun read_file_node file_node master_dir pos src_path = let val _ = Position.report pos Markup.language_path; val _ = (case try Url.explode file_node of NONE => () | SOME (Url.File _) => () | _ => error ("Prover cannot load remote file " ^ Markup.markup (Markup.path file_node) (quote file_node))); val full_path = File.check_file (File.full_path master_dir src_path); val text = File.read full_path; val lines = split_lines text; val digest = SHA1.digest text; val file_pos = Position.copy_id pos (Path.position full_path); in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end handle ERROR msg => error (msg ^ Position.here pos); val read_file = read_file_node ""; local fun blob_file src_path lines digest file_node = let val file_pos = Position.file file_node |> (case Position.get_id (Position.thread_data ()) of NONE => I | SOME exec_id => Position.put_id exec_id); in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end fun resolve_files keywords master_dir (blobs, blobs_index) toks = (case Outer_Syntax.parse_spans toks of [Command_Span.Span (Command_Span.Command_Span (cmd, _), _)] => (case try (nth toks) blobs_index of SOME tok => let val pos = Token.pos_of tok; val path = Path.explode (Token.content_of tok) handle ERROR msg => error (msg ^ Position.here pos); fun make_file src_path (Exn.Res (file_node, NONE)) = Exn.interruptible_capture (fn () => read_file_node file_node master_dir pos src_path) () | make_file src_path (Exn.Res (file_node, SOME (digest, lines))) = (Position.report pos Markup.language_path; Exn.Res (blob_file src_path lines digest file_node)) | make_file _ (Exn.Exn e) = Exn.Exn e; val src_paths = Keyword.command_files keywords cmd path; val files = if null blobs then map2 make_file src_paths (map (K (Exn.Res ("", NONE))) src_paths) else if length src_paths = length blobs then map2 make_file src_paths blobs else error ("Misalignment of inlined files" ^ Position.here pos); in toks |> map_index (fn (i, tok) => if i = blobs_index then Token.put_files files tok else tok) end | NONE => toks) | _ => toks); fun reports_of_token keywords tok = let val malformed_symbols = Input.source_explode (Token.input_of tok) |> map_filter (fn (sym, pos) => if Symbol.is_malformed sym then SOME ((pos, Markup.bad ()), "Malformed symbolic character") else NONE); val is_malformed = Token.is_error tok orelse not (null malformed_symbols); val reports = Token.reports keywords tok @ Token.completion_report tok @ malformed_symbols; in (is_malformed, reports) end; in fun read_thy st = Toplevel.theory_of st handle Toplevel.UNDEF => Pure_Syn.bootstrap_thy; fun read keywords thy master_dir init blobs_info span = let val command_reports = Outer_Syntax.command_reports thy; val core_range = Token.range_of (drop_suffix Token.is_ignored span); val pos = (case find_first Token.is_command span of SOME tok => Token.pos_of tok | NONE => #1 core_range); val token_reports = map (reports_of_token keywords) span; val _ = Position.reports_text (maps #2 token_reports @ maps command_reports span); val verbatim = span |> map_filter (fn tok => if Token.kind_of tok = Token.Verbatim then SOME (Token.pos_of tok) else NONE); val _ = if null verbatim then () else legacy_feature ("Old-style {* verbatim *} token -- use \cartouche\ instead" ^ Position.here_list verbatim); in if exists #1 token_reports then Toplevel.malformed pos "Malformed command syntax" - else - (case Outer_Syntax.parse_tokens thy (resolve_files keywords master_dir blobs_info span) of - [tr] => Toplevel.modify_init init tr - | [] => Toplevel.ignored (#1 (Token.range_of span)) - | _ => Toplevel.malformed (#1 core_range) "Exactly one command expected") - handle ERROR msg => Toplevel.malformed (#1 core_range) msg + else Outer_Syntax.parse_span thy init (resolve_files keywords master_dir blobs_info span) end; end; (* eval *) type eval_state = {failed: bool, command: Toplevel.transition, state: Toplevel.state}; fun init_eval_state opt_thy = {failed = false, command = Toplevel.empty, state = (case opt_thy of NONE => Toplevel.init_toplevel () | SOME thy => Toplevel.theory_toplevel thy)}; datatype eval = Eval of {command_id: Document_ID.command, exec_id: Document_ID.exec, eval_process: eval_state lazy}; fun eval_command_id (Eval {command_id, ...}) = command_id; fun eval_exec_id (Eval {exec_id, ...}) = exec_id; val eval_eq = op = o apply2 eval_exec_id; val eval_running = Execution.is_running_exec o eval_exec_id; fun eval_finished (Eval {eval_process, ...}) = Lazy.is_finished eval_process; fun eval_result (Eval {eval_process, ...}) = Exn.release (Lazy.finished_result eval_process); val eval_result_command = #command o eval_result; val eval_result_state = #state o eval_result; local fun reset_state keywords tr st0 = Toplevel.setmp_thread_position tr (fn () => let val name = Toplevel.name_of tr; val res = if Keyword.is_theory_body keywords name then Toplevel.reset_theory st0 else if Keyword.is_proof keywords name then Toplevel.reset_proof st0 else if Keyword.is_theory_end keywords name then (case Toplevel.reset_notepad st0 of NONE => Toplevel.reset_theory st0 | some => some) else NONE; in (case res of NONE => st0 | SOME st => (Output.error_message (Toplevel.type_error tr ^ " -- using reset state"); st)) end) (); fun run keywords int tr st = if Future.proofs_enabled 1 andalso Keyword.is_diag keywords (Toplevel.name_of tr) then let val (tr1, tr2) = Toplevel.fork_presentation tr; val _ = Execution.fork {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1} (fn () => Toplevel.command_exception int tr1 st); in Toplevel.command_errors int tr2 st end else Toplevel.command_errors int tr st; fun check_token_comments ctxt tok = (Thy_Output.check_comments ctxt (Input.source_explode (Token.input_of tok)); []) handle exn => if Exn.is_interrupt exn then Exn.reraise exn else Runtime.exn_messages exn; fun check_span_comments ctxt span tr = Toplevel.setmp_thread_position tr (fn () => maps (check_token_comments ctxt) span) (); fun report tr m = Toplevel.setmp_thread_position tr (fn () => Output.report [Markup.markup_only m]) (); fun status tr m = Toplevel.setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) (); fun command_indent tr st = (case try Toplevel.proof_of st of SOME prf => let val keywords = Thy_Header.get_keywords (Proof.theory_of prf) in if Keyword.command_kind keywords (Toplevel.name_of tr) = SOME Keyword.prf_script then (case try Proof.goal prf of SOME {goal, ...} => let val n = Thm.nprems_of goal in if n > 1 then report tr (Markup.command_indent (n - 1)) else () end | NONE => ()) else () end | NONE => ()); fun eval_state keywords span tr ({state, ...}: eval_state) = let val _ = Thread_Attributes.expose_interrupt (); val st = reset_state keywords tr state; val _ = command_indent tr st; val _ = status tr Markup.running; val (errs1, result) = run keywords true tr st; val errs2 = (case result of NONE => [] | SOME st' => (case try Toplevel.presentation_context st' of NONE => [] | SOME ctxt' => check_span_comments ctxt' span tr)); val errs = errs1 @ errs2; val _ = List.app (Future.error_message (Toplevel.pos_of tr)) errs; in (case result of NONE => let val _ = status tr Markup.failed; val _ = status tr Markup.finished; val _ = if null errs then (status tr Markup.canceled; Exn.interrupt ()) else (); in {failed = true, command = tr, state = st} end | SOME st' => let val _ = if Keyword.is_theory_end keywords (Toplevel.name_of tr) andalso can (Toplevel.end_theory Position.none) st' then status tr Markup.finalized else (); val _ = status tr Markup.finished; in {failed = false, command = tr, state = st'} end) end; in fun eval keywords master_dir init blobs_info command_id span eval0 = let val exec_id = Document_ID.make (); fun process () = let val eval_state0 = eval_result eval0; val thy = read_thy (#state eval_state0); val tr = Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id)) (fn () => read keywords thy master_dir init blobs_info span |> Toplevel.exec_id exec_id) (); in eval_state keywords span tr eval_state0 end; in Eval {command_id = command_id, exec_id = exec_id, eval_process = Lazy.lazy_name "Command.eval" process} end; end; (* print *) datatype print = Print of {name: string, args: string list, delay: Time.time option, pri: int, persistent: bool, exec_id: Document_ID.exec, print_process: unit lazy}; fun print_exec_id (Print {exec_id, ...}) = exec_id; val print_eq = op = o apply2 print_exec_id; type print_fn = Toplevel.transition -> Toplevel.state -> unit; type print_function = {keywords: Keyword.keywords, command_name: string, args: string list, exec_id: Document_ID.exec} -> {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option; local val print_functions = Synchronized.var "Command.print_functions" ([]: (string * print_function) list); fun print_error tr opt_context e = (Toplevel.setmp_thread_position tr o Runtime.controlled_execution opt_context) e () handle exn => if Exn.is_interrupt exn then Exn.reraise exn else List.app (Future.error_message (Toplevel.pos_of tr)) (Runtime.exn_messages exn); fun print_finished (Print {print_process, ...}) = Lazy.is_finished print_process; fun print_persistent (Print {persistent, ...}) = persistent; val overlay_ord = prod_ord string_ord (list_ord string_ord); fun make_print (name, args) {delay, pri, persistent, strict, print_fn} eval = let val exec_id = Document_ID.make (); fun process () = let val {failed, command, state = st', ...} = eval_result eval; val tr = Toplevel.exec_id exec_id command; val opt_context = try Toplevel.generic_theory_of st'; in if failed andalso strict then () else print_error tr opt_context (fn () => print_fn tr st') end; in Print { name = name, args = args, delay = delay, pri = pri, persistent = persistent, exec_id = exec_id, print_process = Lazy.lazy_name "Command.print" process} end; fun bad_print name_args exn = make_print name_args {delay = NONE, pri = 0, persistent = false, strict = false, print_fn = fn _ => fn _ => Exn.reraise exn}; in fun print0 {pri, print_fn} = make_print ("", [serial_string ()]) {delay = NONE, pri = pri, persistent = true, strict = true, print_fn = print_fn}; fun print command_visible command_overlays keywords command_name eval old_prints = let val print_functions = Synchronized.value print_functions; fun new_print (name, args) get_pr = let val params = {keywords = keywords, command_name = command_name, args = args, exec_id = eval_exec_id eval}; in (case Exn.capture (Runtime.controlled_execution NONE get_pr) params of Exn.Res NONE => NONE | Exn.Res (SOME pr) => SOME (make_print (name, args) pr eval) | Exn.Exn exn => SOME (bad_print (name, args) exn eval)) end; fun get_print (name, args) = (case find_first (fn Print print => (#name print, #args print) = (name, args)) old_prints of NONE => (case AList.lookup (op =) print_functions name of NONE => SOME (bad_print (name, args) (ERROR ("Missing print function " ^ quote name)) eval) | SOME get_pr => new_print (name, args) get_pr) | some => some); val retained_prints = filter (fn print => print_finished print andalso print_persistent print) old_prints; val visible_prints = if command_visible then fold (fn (name, _) => cons (name, [])) print_functions command_overlays |> sort_distinct overlay_ord |> map_filter get_print else []; val new_prints = visible_prints @ retained_prints; in if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints end; fun parallel_print (Print {pri, ...}) = pri <= 0 orelse (Future.enabled () andalso Options.default_bool "parallel_print"); fun print_function name f = Synchronized.change print_functions (fn funs => (if name = "" then error "Unnamed print function" else (); if not (AList.defined (op =) funs name) then () else warning ("Redefining command print function: " ^ quote name); AList.update (op =) (name, f) funs)); fun no_print_function name = Synchronized.change print_functions (filter_out (equal name o #1)); end; val _ = print_function "Execution.print" (fn {args, exec_id, ...} => if null args then SOME {delay = NONE, pri = Task_Queue.urgent_pri + 2, persistent = false, strict = false, print_fn = fn _ => fn _ => Execution.fork_prints exec_id} else NONE); val _ = print_function "print_state" (fn {keywords, command_name, ...} => if Options.default_bool "editor_output_state" andalso Keyword.is_printed keywords command_name then SOME {delay = NONE, pri = Task_Queue.urgent_pri + 1, persistent = false, strict = false, print_fn = fn _ => fn st => if Toplevel.is_proof st then Output.state (Toplevel.string_of_state st) else ()} else NONE); (* combined execution *) type exec = eval * print list; fun init_exec opt_thy : exec = (Eval {command_id = Document_ID.none, exec_id = Document_ID.none, eval_process = Lazy.value (init_eval_state opt_thy)}, []); val no_exec = init_exec NONE; fun exec_ids NONE = [] | exec_ids (SOME (eval, prints)) = eval_exec_id eval :: map print_exec_id prints; local fun run_process execution_id exec_id process = let val group = Future.worker_subgroup () in if Execution.running execution_id exec_id [group] then ignore (task_context group (fn () => Lazy.force_result {strict = true} process) ()) else () end; fun ignore_process process = Lazy.is_running process orelse Lazy.is_finished process; fun run_eval execution_id (Eval {exec_id, eval_process, ...}) = if Lazy.is_finished eval_process then () else run_process execution_id exec_id eval_process; fun fork_print execution_id deps (Print {name, delay, pri, exec_id, print_process, ...}) = let val group = Future.worker_subgroup (); fun fork () = ignore ((singleton o Future.forks) {name = name, group = SOME group, deps = deps, pri = pri, interrupts = true} (fn () => if ignore_process print_process then () else run_process execution_id exec_id print_process)); in (case delay of NONE => fork () | SOME d => ignore (Event_Timer.request {physical = true} (Time.now () + d) fork)) end; fun run_print execution_id (print as Print {exec_id, print_process, ...}) = if ignore_process print_process then () else if parallel_print print then fork_print execution_id [] print else run_process execution_id exec_id print_process; in fun exec execution_id (eval, prints) = (run_eval execution_id eval; List.app (run_print execution_id) prints); fun exec_parallel_prints execution_id deps (exec as (Eval {eval_process, ...}, prints)) = if Lazy.is_finished eval_process then (List.app (fork_print execution_id deps) prints; NONE) else SOME exec; end; end; diff --git a/src/Pure/PIDE/command.scala b/src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala +++ b/src/Pure/PIDE/command.scala @@ -1,636 +1,635 @@ /* Title: Pure/PIDE/command.scala Author: Fabian Immler, TU Munich Author: Makarius Prover commands with accumulated results from execution. */ package isabelle import scala.collection.mutable import scala.collection.immutable.SortedMap object Command { type Edit = (Option[Command], Option[Command]) type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, Symbol.Text_Chunk)])] type Blobs_Info = (List[Blob], Int) val no_blobs: Blobs_Info = (Nil, -1) /** accumulated results from prover **/ /* results */ object Results { type Entry = (Long, XML.Tree) val empty: Results = new Results(SortedMap.empty) def make(args: TraversableOnce[Results.Entry]): Results = (empty /: args)(_ + _) def merge(args: TraversableOnce[Results]): Results = (empty /: args)(_ ++ _) /* XML data representation */ val encode: XML.Encode.T[Results] = (results: Results) => { import XML.Encode._; list(pair(long, tree))(results.rep.toList) } val decode: XML.Decode.T[Results] = (body: XML.Body) => { import XML.Decode._; make(list(pair(long, tree))(body)) } } final class Results private(private val rep: SortedMap[Long, XML.Tree]) { def is_empty: Boolean = rep.isEmpty def defined(serial: Long): Boolean = rep.isDefinedAt(serial) def get(serial: Long): Option[XML.Tree] = rep.get(serial) def iterator: Iterator[Results.Entry] = rep.iterator def + (entry: Results.Entry): Results = if (defined(entry._1)) this else new Results(rep + entry) def ++ (other: Results): Results = if (this eq other) this else if (rep.isEmpty) other else (this /: other.iterator)(_ + _) override def hashCode: Int = rep.hashCode override def equals(that: Any): Boolean = that match { case other: Results => rep == other.rep case _ => false } override def toString: String = iterator.mkString("Results(", ", ", ")") } /* exports */ object Exports { type Entry = (Long, Export.Entry) val empty: Exports = new Exports(SortedMap.empty) def merge(args: TraversableOnce[Exports]): Exports = (empty /: args)(_ ++ _) } final class Exports private(private val rep: SortedMap[Long, Export.Entry]) { def is_empty: Boolean = rep.isEmpty def iterator: Iterator[Exports.Entry] = rep.iterator def + (entry: Exports.Entry): Exports = if (rep.isDefinedAt(entry._1)) this else new Exports(rep + entry) def ++ (other: Exports): Exports = if (this eq other) this else if (rep.isEmpty) other else (this /: other.iterator)(_ + _) override def hashCode: Int = rep.hashCode override def equals(that: Any): Boolean = that match { case other: Exports => rep == other.rep case _ => false } override def toString: String = iterator.mkString("Exports(", ", ", ")") } /* markups */ object Markup_Index { val markup: Markup_Index = Markup_Index(false, Symbol.Text_Chunk.Default) } sealed case class Markup_Index(status: Boolean, chunk_name: Symbol.Text_Chunk.Name) object Markups { val empty: Markups = new Markups(Map.empty) def init(markup: Markup_Tree): Markups = new Markups(Map(Markup_Index.markup -> markup)) def merge(args: TraversableOnce[Markups]): Markups = (empty /: args)(_ ++ _) /* XML data representation */ def encode(source_length: Int): XML.Encode.T[Markups] = (markups: Markups) => { import XML.Encode._ val markup_index: T[Markup_Index] = (index: Markup_Index) => pair(bool, Symbol.Text_Chunk.encode_name)(index.status, index.chunk_name) val markup_tree: T[Markup_Tree] = _.to_XML(Text.Range(0, source_length), Symbol.spaces(source_length), Markup.Elements.full) list(pair(markup_index, markup_tree))(markups.rep.toList) } val decode: XML.Decode.T[Markups] = (body: XML.Body) => { import XML.Decode._ val markup_index: T[Markup_Index] = (body: XML.Body) => { val (status, chunk_name) = pair(bool, Symbol.Text_Chunk.decode_name)(body) Markup_Index(status, chunk_name) } (Markups.empty /: list(pair(markup_index, Markup_Tree.from_XML(_)))(body))(_ + _) } } final class Markups private(private val rep: Map[Markup_Index, Markup_Tree]) { def is_empty: Boolean = rep.isEmpty def apply(index: Markup_Index): Markup_Tree = rep.getOrElse(index, Markup_Tree.empty) def add(index: Markup_Index, markup: Text.Markup): Markups = new Markups(rep + (index -> (this(index) + markup))) def + (entry: (Markup_Index, Markup_Tree)): Markups = { val (index, tree) = entry new Markups(rep + (index -> (this(index).merge(tree, Text.Range.full, Markup.Elements.full)))) } def ++ (other: Markups): Markups = if (this eq other) this else if (rep.isEmpty) other else (this /: other.rep.iterator)(_ + _) def redirection_iterator: Iterator[Document_ID.Generic] = for (Markup_Index(_, Symbol.Text_Chunk.Id(id)) <- rep.keysIterator) yield id def redirect(other_id: Document_ID.Generic): Markups = { val rep1 = (for { (Markup_Index(status, Symbol.Text_Chunk.Id(id)), markup) <- rep.iterator if other_id == id } yield (Markup_Index(status, Symbol.Text_Chunk.Default), markup)).toMap if (rep1.isEmpty) Markups.empty else new Markups(rep1) } override def hashCode: Int = rep.hashCode override def equals(that: Any): Boolean = that match { case other: Markups => rep == other.rep case _ => false } override def toString: String = rep.iterator.mkString("Markups(", ", ", ")") } /* state */ object State { def get_result(states: List[State], serial: Long): Option[XML.Tree] = states.find(st => st.results.defined(serial)).map(st => st.results.get(serial).get) def get_result_proper(states: List[State], props: Properties.T): Option[Results.Entry] = for { serial <- Markup.Serial.unapply(props) tree @ XML.Elem(_, body) <- get_result(states, serial) if body.nonEmpty } yield (serial -> tree) def merge_results(states: List[State]): Results = Results.merge(states.map(_.results)) def merge_exports(states: List[State]): Exports = Exports.merge(states.map(_.exports)) def merge_markups(states: List[State]): Markups = Markups.merge(states.map(_.markups)) def merge_markup(states: List[State], index: Markup_Index, range: Text.Range, elements: Markup.Elements): Markup_Tree = Markup_Tree.merge(states.map(_.markup(index)), range, elements) def merge(command: Command, states: List[State]): State = State(command, states.flatMap(_.status), merge_results(states), merge_exports(states), merge_markups(states)) /* XML data representation */ val encode: XML.Encode.T[State] = (st: State) => { import XML.Encode._ val command = st.command val blobs_names = command.blobs_names.map(_.node) val blobs_index = command.blobs_index require(command.blobs_ok) pair(long, pair(string, pair(pair(list(string), int), pair(Command_Span.encode, pair(list(Markup.encode), pair(Results.encode, Markups.encode(command.source.length)))))))( (command.id, (command.node_name.node, ((blobs_names, blobs_index), (command.span, (st.status, (st.results, st.markups))))))) } def decode(node_name: String => Document.Node.Name): XML.Decode.T[State] = (body: XML.Body) => { import XML.Decode._ val (id, (node, ((blobs_names, blobs_index), (span, (status, (results, markups)))))) = pair(long, pair(string, pair(pair(list(string), int), pair(Command_Span.decode, pair(list(Markup.decode), pair(Results.decode, Markups.decode))))))(body) val blobs_info: Blobs_Info = (blobs_names.map(name => Exn.Res((node_name(name), None)): Blob), blobs_index) val command = Command(id, node_name(node), blobs_info, span) State(command, status, results, Exports.empty, markups) } } sealed case class State( command: Command, status: List[Markup] = Nil, results: Results = Results.empty, exports: Exports = Exports.empty, markups: Markups = Markups.empty) { def initialized: Boolean = status.exists(markup => markup.name == Markup.INITIALIZED) def consolidated: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATED) lazy val maybe_consolidated: Boolean = { var touched = false var forks = 0 var runs = 0 for (markup <- status) { markup.name match { case Markup.FORKED => touched = true; forks += 1 case Markup.JOINED => forks -= 1 case Markup.RUNNING => touched = true; runs += 1 case Markup.FINISHED => runs -= 1 case _ => } } touched && forks == 0 && runs == 0 } lazy val document_status: Document_Status.Command_Status = { val warnings = if (results.iterator.exists(p => Protocol.is_warning(p._2) || Protocol.is_legacy(p._2))) List(Markup(Markup.WARNING, Nil)) else Nil val errors = if (results.iterator.exists(p => Protocol.is_error(p._2))) List(Markup(Markup.ERROR, Nil)) else Nil Document_Status.Command_Status.make((warnings ::: errors ::: status).iterator) } def markup(index: Markup_Index): Markup_Tree = markups(index) def redirect(other_command: Command): Option[State] = { val markups1 = markups.redirect(other_command.id) if (markups1.is_empty) None else Some(new State(other_command, markups = markups1)) } private def add_status(st: Markup): State = copy(status = st :: status) private def add_result(entry: Results.Entry): State = copy(results = results + entry) def add_export(entry: Exports.Entry): Option[State] = if (command.node_name.theory == entry._2.theory_name) Some(copy(exports = exports + entry)) else None private def add_markup( status: Boolean, chunk_name: Symbol.Text_Chunk.Name, m: Text.Markup): State = { val markups1 = if (status || Document_Status.Command_Status.liberal_elements(m.info.name)) markups.add(Markup_Index(true, chunk_name), m) else markups copy(markups = markups1.add(Markup_Index(false, chunk_name), m)) } def accumulate( self_id: Document_ID.Generic => Boolean, other_id: Document_ID.Generic => Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)], message: XML.Elem, xml_cache: XML.Cache): State = message match { case XML.Elem(Markup(Markup.STATUS, _), msgs) => (this /: msgs)((state, msg) => msg match { case elem @ XML.Elem(markup, Nil) => state. add_status(markup). add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.core_range, elem)) case _ => Output.warning("Ignored status message: " + msg) state }) case XML.Elem(Markup(Markup.REPORT, _), msgs) => (this /: msgs)((state, msg) => { def bad(): Unit = Output.warning("Ignored report message: " + msg) msg match { case XML.Elem(Markup(name, atts @ Position.Identified(id, chunk_name)), args) => val target = if (self_id(id) && command.chunks.isDefinedAt(chunk_name)) Some((chunk_name, command.chunks(chunk_name))) else if (chunk_name == Symbol.Text_Chunk.Default) other_id(id) else None (target, atts) match { case (Some((target_name, target_chunk)), Position.Range(symbol_range)) => target_chunk.incorporate(symbol_range) match { case Some(range) => val props = Position.purge(atts) val elem = xml_cache.elem(XML.Elem(Markup(name, props), args)) state.add_markup(false, target_name, Text.Info(range, elem)) case None => bad(); state } case _ => // silently ignore excessive reports state } case XML.Elem(Markup(name, atts), args) if !atts.exists({ case (a, _) => Markup.POSITION_PROPERTIES(a) }) => val range = command.core_range val props = Position.purge(atts) val elem = xml_cache.elem(XML.Elem(Markup(name, props), args)) state.add_markup(false, Symbol.Text_Chunk.Default, Text.Info(range, elem)) case _ => bad(); state } }) case XML.Elem(Markup(name, props), body) => props match { case Markup.Serial(i) => val markup_message = xml_cache.elem(XML.Elem(Markup(Markup.message(name), props), body)) val message_markup = xml_cache.elem(XML.elem(Markup(name, props.filter(p => p._1 == Markup.SERIAL)))) var st = add_result(i -> markup_message) if (Protocol.is_inlined(message)) { for { (chunk_name, chunk) <- command.chunks.iterator range <- Protocol_Message.positions( self_id, command.span.position, chunk_name, chunk, message) } st = st.add_markup(false, chunk_name, Text.Info(range, message_markup)) } st case _ => Output.warning("Ignored message without serial number: " + message) this } } } /** static content **/ /* make commands */ def apply( id: Document_ID.Command, node_name: Document.Node.Name, blobs_info: Blobs_Info, span: Command_Span.Span): Command = { val (source, span1) = span.compact_source new Command(id, node_name, blobs_info, span1, source, Results.empty, Markup_Tree.empty) } val empty: Command = Command(Document_ID.none, Document.Node.Name.empty, no_blobs, Command_Span.empty) def unparsed( id: Document_ID.Command, source: String, results: Results, markup: Markup_Tree): Command = { val (source1, span1) = Command_Span.unparsed(source).compact_source new Command(id, Document.Node.Name.empty, no_blobs, span1, source1, results, markup) } def text(source: String): Command = unparsed(Document_ID.none, source, Results.empty, Markup_Tree.empty) def rich_text(id: Document_ID.Command, results: Results, body: XML.Body): Command = { val text = XML.content(body) val markup = Markup_Tree.from_XML(body) unparsed(id, text, results, markup) } /* perspective */ object Perspective { val empty: Perspective = Perspective(Nil) } sealed case class Perspective(commands: List[Command]) // visible commands in canonical order { def is_empty: Boolean = commands.isEmpty def same(that: Perspective): Boolean = { val cmds1 = this.commands val cmds2 = that.commands require(!cmds1.exists(_.is_undefined)) require(!cmds2.exists(_.is_undefined)) cmds1.length == cmds2.length && (cmds1.iterator zip cmds2.iterator).forall({ case (c1, c2) => c1.id == c2.id }) } } /* blobs: inlined errors and auxiliary files */ private def clean_tokens(tokens: List[Token]): List[(Token, Int)] = { def clean(toks: List[(Token, Int)]): List[(Token, Int)] = toks match { case (t1, i1) :: (t2, i2) :: rest => if (t1.is_keyword && t1.source == "%" && t2.is_name) clean(rest) - else if (t1.is_keyword && Symbol.is_marker(t1.source) && t2.is_embedded) clean(rest) else (t1, i1) :: clean((t2, i2) :: rest) case _ => toks } clean(tokens.zipWithIndex.filter({ case (t, _) => t.is_proper })) } private def find_file(tokens: List[(Token, Int)]): Option[(String, Int)] = if (tokens.exists({ case (t, _) => t.is_command })) { tokens.dropWhile({ case (t, _) => !t.is_command }). collectFirst({ case (t, i) if t.is_embedded => (t.content, i) }) } else None def span_files(syntax: Outer_Syntax, span: Command_Span.Span): (List[String], Int) = syntax.load_command(span.name) match { case Some(exts) => find_file(clean_tokens(span.content)) match { case Some((file, i)) => if (exts.isEmpty) (List(file), i) else (exts.map(ext => file + "." + ext), i) case None => (Nil, -1) } case None => (Nil, -1) } def blobs_info( resources: Resources, syntax: Outer_Syntax, get_blob: Document.Node.Name => Option[Document.Blob], can_import: Document.Node.Name => Boolean, node_name: Document.Node.Name, span: Command_Span.Span): Blobs_Info = { span.name match { // inlined errors case Thy_Header.THEORY => val reader = Scan.char_reader(Token.implode(span.content)) val imports = resources.check_thy_reader(node_name, reader).imports val raw_imports = try { val imports1 = Thy_Header.read(reader, Token.Pos.none).imports if (imports.length == imports1.length) imports1.map(_._1) else error("") } catch { case exn: Throwable => List.fill(imports.length)("") } val errors = for { ((import_name, pos), s) <- imports zip raw_imports if !can_import(import_name) } yield { val completion = if (Thy_Header.is_base_name(s)) { val completed = Completion.completed(import_name.theory_base_name) val qualifier = resources.session_base.theory_qualifier(node_name) val dir = node_name.master_dir for { known_name <- resources.session_base.known.theory_names if completed(known_name.theory_base_name) } yield { resources.standard_import( resources.session_base, qualifier, dir, known_name.theory) } }.sorted else Nil val msg = "Bad theory import " + Markup.Path(import_name.node).markup(quote(import_name.toString)) + Position.here(pos) + Completion.report_theories(pos, completion) Exn.Exn(ERROR(msg)): Command.Blob } (errors, -1) // auxiliary files case _ => val (files, index) = span_files(syntax, span) val blobs = files.map(file => (Exn.capture { val name = Document.Node.Name(resources.append(node_name, Path.explode(file))) val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk))) (name, blob) }).user_error) (blobs, index) } } } final class Command private( val id: Document_ID.Command, val node_name: Document.Node.Name, val blobs_info: Command.Blobs_Info, val span: Command_Span.Span, val source: String, val init_results: Command.Results, val init_markup: Markup_Tree) { override def toString: String = id + "/" + span.kind.toString /* classification */ def is_proper: Boolean = span.kind.isInstanceOf[Command_Span.Command_Span] def is_ignored: Boolean = span.kind == Command_Span.Ignored_Span def is_undefined: Boolean = id == Document_ID.none val is_unparsed: Boolean = span.content.exists(_.is_unparsed) val is_unfinished: Boolean = span.content.exists(_.is_unfinished) def potentially_initialized: Boolean = span.name == Thy_Header.THEORY /* blobs */ def blobs: List[Command.Blob] = blobs_info._1 def blobs_index: Int = blobs_info._2 def blobs_ok: Boolean = blobs.forall({ case Exn.Res(_) => true case _ => false }) def blobs_names: List[Document.Node.Name] = for (Exn.Res((name, _)) <- blobs) yield name def blobs_undefined: List[Document.Node.Name] = for (Exn.Res((name, None)) <- blobs) yield name def blobs_defined: List[(Document.Node.Name, SHA1.Digest)] = for (Exn.Res((name, Some((digest, _)))) <- blobs) yield (name, digest) def blobs_changed(doc_blobs: Document.Blobs): Boolean = blobs.exists({ case Exn.Res((name, _)) => doc_blobs.changed(name) case _ => false }) /* source chunks */ val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(source) val chunks: Map[Symbol.Text_Chunk.Name, Symbol.Text_Chunk] = ((Symbol.Text_Chunk.Default -> chunk) :: (for (Exn.Res((name, Some((_, file)))) <- blobs) yield Symbol.Text_Chunk.File(name.node) -> file)).toMap def length: Int = source.length def range: Text.Range = chunk.range val core_range: Text.Range = Text.Range(0, (length /: span.content.reverse.iterator.takeWhile(_.is_ignored))(_ - _.source.length)) def source(range: Text.Range): String = range.substring(source) /* accumulated results */ val init_state: Command.State = Command.State(this, results = init_results, markups = Command.Markups.init(init_markup)) val empty_state: Command.State = Command.State(this) } diff --git a/src/Pure/Pure.thy b/src/Pure/Pure.thy --- a/src/Pure/Pure.thy +++ b/src/Pure/Pure.thy @@ -1,1475 +1,1475 @@ (* Title: Pure/Pure.thy Author: Makarius The Pure theory, with definitions of Isar commands and some lemmas. *) theory Pure keywords "!!" "!" "+" ":" ";" "<" "<=" "==" "=>" "?" "[" "\" "\" "\" "\" "\" - "\" "\" "]" "binder" "in" "infix" "infixl" "infixr" "is" "open" "output" + "\" "]" "binder" "in" "infix" "infixl" "infixr" "is" "open" "output" "overloaded" "pervasive" "premises" "structure" "unchecked" and "private" "qualified" :: before_command and "assumes" "constrains" "defines" "fixes" "for" "if" "includes" "notes" "rewrites" "obtains" "shows" "when" "where" "|" :: quasi_command and "text" "txt" :: document_body and "text_raw" :: document_raw and "default_sort" :: thy_decl and "typedecl" "type_synonym" "nonterminal" "judgment" "consts" "syntax" "no_syntax" "translations" "no_translations" "definition" "abbreviation" "type_notation" "no_type_notation" "notation" "no_notation" "axiomatization" "alias" "type_alias" "lemmas" "declare" "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl and "external_file" "bibtex_file" :: thy_load and "generate_file" :: thy_decl and "export_generated_files" :: diag and "ML_file" "ML_file_debug" "ML_file_no_debug" :: thy_load % "ML" and "SML_file" "SML_file_debug" "SML_file_no_debug" :: thy_load % "ML" and "SML_import" "SML_export" "ML_export" :: thy_decl % "ML" and "ML_prf" :: prf_decl % "proof" (* FIXME % "ML" ?? *) and "ML_val" "ML_command" :: diag % "ML" and "simproc_setup" :: thy_decl % "ML" and "setup" "local_setup" "attribute_setup" "method_setup" "declaration" "syntax_declaration" "parse_ast_translation" "parse_translation" "print_translation" "typed_print_translation" "print_ast_translation" "oracle" :: thy_decl % "ML" and "bundle" :: thy_decl_block and "unbundle" :: thy_decl and "include" "including" :: prf_decl and "print_bundles" :: diag and "context" "locale" "experiment" :: thy_decl_block and "interpret" :: prf_goal % "proof" and "interpretation" "global_interpretation" "sublocale" :: thy_goal and "class" :: thy_decl_block and "subclass" :: thy_goal and "instantiation" :: thy_decl_block and "instance" :: thy_goal and "overloading" :: thy_decl_block and "code_datatype" :: thy_decl and "theorem" "lemma" "corollary" "proposition" :: thy_goal and "schematic_goal" :: thy_goal and "notepad" :: thy_decl_block and "have" :: prf_goal % "proof" and "hence" :: prf_goal % "proof" and "show" :: prf_asm_goal % "proof" and "thus" :: prf_asm_goal % "proof" and "then" "from" "with" :: prf_chain % "proof" and "note" :: prf_decl % "proof" and "supply" :: prf_script % "proof" and "using" "unfolding" :: prf_decl % "proof" and "fix" "assume" "presume" "define" :: prf_asm % "proof" and "consider" :: prf_goal % "proof" and "obtain" :: prf_asm_goal % "proof" and "guess" :: prf_script_asm_goal % "proof" and "let" "write" :: prf_decl % "proof" and "case" :: prf_asm % "proof" and "{" :: prf_open % "proof" and "}" :: prf_close % "proof" and "next" :: next_block % "proof" and "qed" :: qed_block % "proof" and "by" ".." "." "sorry" "\" :: "qed" % "proof" and "done" :: "qed_script" % "proof" and "oops" :: qed_global % "proof" and "defer" "prefer" "apply" :: prf_script % "proof" and "apply_end" :: prf_script % "proof" and "subgoal" :: prf_script_goal % "proof" and "proof" :: prf_block % "proof" and "also" "moreover" :: prf_decl % "proof" and "finally" "ultimately" :: prf_chain % "proof" and "back" :: prf_script % "proof" and "help" "print_commands" "print_options" "print_context" "print_theory" "print_definitions" "print_syntax" "print_abbrevs" "print_defn_rules" "print_theorems" "print_locales" "print_classes" "print_locale" "print_interps" "print_dependencies" "print_attributes" "print_simpset" "print_rules" "print_trans_rules" "print_methods" "print_antiquotations" "print_ML_antiquotations" "thy_deps" "locale_deps" "class_deps" "thm_deps" "print_term_bindings" "print_facts" "print_cases" "print_statement" "thm" "prf" "full_prf" "prop" "term" "typ" "print_codesetup" "unused_thms" :: diag and "print_state" :: diag and "welcome" :: diag and "end" :: thy_end and "realizers" :: thy_decl and "realizability" :: thy_decl and "extract_type" "extract" :: thy_decl and "find_theorems" "find_consts" :: diag and "named_theorems" :: thy_decl abbrevs "===>" = "===>" (*prevent replacement of very long arrows*) and "--->" = "\\" and "hence" "thus" "default_sort" "simproc_setup" "apply_end" "realizers" "realizability" = "" and "hence" = "then have" and "thus" = "then show" begin section \Isar commands\ subsection \Other files\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\external_file\ "formal dependency on external file" (Resources.provide_parse_files "external_file" >> (fn files => Toplevel.theory (#2 o files))); val _ = Outer_Syntax.command \<^command_keyword>\bibtex_file\ "check bibtex database file in Prover IDE" (Resources.provide_parse_files "bibtex_file" >> (fn files => Toplevel.theory (fn thy => let val ([{lines, pos, ...}], thy') = files thy; val _ = Bibtex.check_database_output pos (cat_lines lines); in thy' end))); val _ = Outer_Syntax.local_theory \<^command_keyword>\generate_file\ "generate source file, with antiquotations" (Parse.position Parse.path -- (\<^keyword>\=\ |-- Parse.input Parse.embedded) >> Generated_Files.generate_file_cmd); val _ = Outer_Syntax.command \<^command_keyword>\export_generated_files\ "export generated files from this or other theories" (Scan.repeat Parse.name_position >> (fn names => Toplevel.keep (fn st => let val ctxt = Toplevel.context_of st; val thy = Toplevel.theory_of st; val other_thys = if null names then [thy] else map (Theory.check {long = false} ctxt) names; val paths = Generated_Files.export_files thy other_thys; in if not (null paths) then (writeln (Export.message thy ""); writeln (cat_lines (paths |> map (fn (path, pos) => Markup.markup (Markup.entityN, Position.def_properties_of pos) (quote (Path.implode path)))))) else () end))); in end\ subsection \Embedded ML text\ ML \ local val semi = Scan.option \<^keyword>\;\; val _ = Outer_Syntax.command \<^command_keyword>\ML_file\ "read and evaluate Isabelle/ML file" (Resources.parse_files "ML_file" --| semi >> ML_File.ML NONE); val _ = Outer_Syntax.command \<^command_keyword>\ML_file_debug\ "read and evaluate Isabelle/ML file (with debugger information)" (Resources.parse_files "ML_file_debug" --| semi >> ML_File.ML (SOME true)); val _ = Outer_Syntax.command \<^command_keyword>\ML_file_no_debug\ "read and evaluate Isabelle/ML file (no debugger information)" (Resources.parse_files "ML_file_no_debug" --| semi >> ML_File.ML (SOME false)); val _ = Outer_Syntax.command \<^command_keyword>\SML_file\ "read and evaluate Standard ML file" (Resources.parse_files "SML_file" --| semi >> ML_File.SML NONE); val _ = Outer_Syntax.command \<^command_keyword>\SML_file_debug\ "read and evaluate Standard ML file (with debugger information)" (Resources.parse_files "SML_file_debug" --| semi >> ML_File.SML (SOME true)); val _ = Outer_Syntax.command \<^command_keyword>\SML_file_no_debug\ "read and evaluate Standard ML file (no debugger information)" (Resources.parse_files "SML_file_no_debug" --| semi >> ML_File.SML (SOME false)); val _ = Outer_Syntax.command \<^command_keyword>\SML_export\ "evaluate SML within Isabelle/ML environment" (Parse.ML_source >> (fn source => let val flags: ML_Compiler.flags = {environment = ML_Env.SML_export, redirect = false, verbose = true, debug = NONE, writeln = writeln, warning = warning}; in Toplevel.theory (Context.theory_map (ML_Context.exec (fn () => ML_Context.eval_source flags source))) end)); val _ = Outer_Syntax.command \<^command_keyword>\SML_import\ "evaluate Isabelle/ML within SML environment" (Parse.ML_source >> (fn source => let val flags: ML_Compiler.flags = {environment = ML_Env.SML_import, redirect = false, verbose = true, debug = NONE, writeln = writeln, warning = warning}; in Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval_source flags source) #> Local_Theory.propagate_ml_env) end)); val _ = Outer_Syntax.command ("ML_export", \<^here>) "ML text within theory or local theory, and export to bootstrap environment" (Parse.ML_source >> (fn source => Toplevel.generic_theory (fn context => context |> Config.put_generic ML_Env.ML_environment ML_Env.Isabelle |> Config.put_generic ML_Env.ML_write_global true |> ML_Context.exec (fn () => ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source) |> Config.restore_generic ML_Env.ML_write_global context |> Config.restore_generic ML_Env.ML_environment context |> Local_Theory.propagate_ml_env))); val _ = Outer_Syntax.command \<^command_keyword>\ML_prf\ "ML text within proof" (Parse.ML_source >> (fn source => Toplevel.proof (Proof.map_context (Context.proof_map (ML_Context.exec (fn () => ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source))) #> Proof.propagate_ml_env))); val _ = Outer_Syntax.command \<^command_keyword>\ML_val\ "diagnostic ML text" (Parse.ML_source >> Isar_Cmd.ml_diag true); val _ = Outer_Syntax.command \<^command_keyword>\ML_command\ "diagnostic ML text (silent)" (Parse.ML_source >> Isar_Cmd.ml_diag false); val _ = Outer_Syntax.command \<^command_keyword>\setup\ "ML setup for global theory" (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.setup)); val _ = Outer_Syntax.local_theory \<^command_keyword>\local_setup\ "ML setup for local theory" (Parse.ML_source >> Isar_Cmd.local_setup); val _ = Outer_Syntax.command \<^command_keyword>\oracle\ "declare oracle" (Parse.range Parse.name -- (\<^keyword>\=\ |-- Parse.ML_source) >> (fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y))); val _ = Outer_Syntax.local_theory \<^command_keyword>\attribute_setup\ "define attribute in ML" (Parse.name_position -- Parse.!!! (\<^keyword>\=\ |-- Parse.ML_source -- Scan.optional Parse.text "") >> (fn (name, (txt, cmt)) => Attrib.attribute_setup name txt cmt)); val _ = Outer_Syntax.local_theory \<^command_keyword>\method_setup\ "define proof method in ML" (Parse.name_position -- Parse.!!! (\<^keyword>\=\ |-- Parse.ML_source -- Scan.optional Parse.text "") >> (fn (name, (txt, cmt)) => Method.method_setup name txt cmt)); val _ = Outer_Syntax.local_theory \<^command_keyword>\declaration\ "generic ML declaration" (Parse.opt_keyword "pervasive" -- Parse.ML_source >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = false, pervasive = pervasive} txt)); val _ = Outer_Syntax.local_theory \<^command_keyword>\syntax_declaration\ "generic ML syntax declaration" (Parse.opt_keyword "pervasive" -- Parse.ML_source >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = true, pervasive = pervasive} txt)); val _ = Outer_Syntax.local_theory \<^command_keyword>\simproc_setup\ "define simproc in ML" (Parse.name_position -- (\<^keyword>\(\ |-- Parse.enum1 "|" Parse.term --| \<^keyword>\)\ --| \<^keyword>\=\) -- Parse.ML_source >> (fn ((a, b), c) => Isar_Cmd.simproc_setup a b c)); in end\ subsection \Theory commands\ subsubsection \Sorts and types\ ML \ local val _ = Outer_Syntax.local_theory \<^command_keyword>\default_sort\ "declare default sort for explicit type variables" (Parse.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy)); val _ = Outer_Syntax.local_theory \<^command_keyword>\typedecl\ "type declaration" (Parse.type_args -- Parse.binding -- Parse.opt_mixfix >> (fn ((args, a), mx) => Typedecl.typedecl {final = true} (a, map (rpair dummyS) args, mx) #> snd)); val _ = Outer_Syntax.local_theory \<^command_keyword>\type_synonym\ "declare type abbreviation" (Parse.type_args -- Parse.binding -- (\<^keyword>\=\ |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix')) >> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs)); in end\ subsubsection \Consts\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\judgment\ "declare object-logic judgment" (Parse.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\consts\ "declare constants" (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts_cmd)); in end\ subsubsection \Syntax and translations\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\nonterminal\ "declare syntactic type constructors (grammar nonterminal symbols)" (Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global)); val _ = Outer_Syntax.command \<^command_keyword>\syntax\ "add raw syntax clauses" (Parse.syntax_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.add_syntax_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\no_syntax\ "delete raw syntax clauses" (Parse.syntax_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.del_syntax_cmd)); val trans_pat = Scan.optional (\<^keyword>\(\ |-- Parse.!!! (Parse.inner_syntax Parse.name --| \<^keyword>\)\)) "logic" -- Parse.inner_syntax Parse.string; fun trans_arrow toks = ((\<^keyword>\\\ || \<^keyword>\=>\) >> K Syntax.Parse_Rule || (\<^keyword>\\\ || \<^keyword>\<=\) >> K Syntax.Print_Rule || (\<^keyword>\\\ || \<^keyword>\==\) >> K Syntax.Parse_Print_Rule) toks; val trans_line = trans_pat -- Parse.!!! (trans_arrow -- trans_pat) >> (fn (left, (arr, right)) => arr (left, right)); val _ = Outer_Syntax.command \<^command_keyword>\translations\ "add syntax translation rules" (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations)); val _ = Outer_Syntax.command \<^command_keyword>\no_translations\ "delete syntax translation rules" (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations)); in end\ subsubsection \Translation functions\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\parse_ast_translation\ "install parse ast translation functions" (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_ast_translation)); val _ = Outer_Syntax.command \<^command_keyword>\parse_translation\ "install parse translation functions" (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_translation)); val _ = Outer_Syntax.command \<^command_keyword>\print_translation\ "install print translation functions" (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_translation)); val _ = Outer_Syntax.command \<^command_keyword>\typed_print_translation\ "install typed print translation functions" (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.typed_print_translation)); val _ = Outer_Syntax.command \<^command_keyword>\print_ast_translation\ "install print ast translation functions" (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_ast_translation)); in end\ subsubsection \Specifications\ ML \ local val _ = Outer_Syntax.local_theory' \<^command_keyword>\definition\ "constant definition" (Scan.option Parse_Spec.constdecl -- (Parse_Spec.opt_thm_name ":" -- Parse.prop) -- Parse_Spec.if_assumes -- Parse.for_fixes >> (fn (((decl, spec), prems), params) => #2 oo Specification.definition_cmd decl params prems spec)); val _ = Outer_Syntax.local_theory' \<^command_keyword>\abbreviation\ "constant abbreviation" (Parse.syntax_mode -- Scan.option Parse_Spec.constdecl -- Parse.prop -- Parse.for_fixes >> (fn (((mode, decl), spec), params) => Specification.abbreviation_cmd mode decl params spec)); val axiomatization = Parse.and_list1 (Parse_Spec.thm_name ":" -- Parse.prop) -- Parse_Spec.if_assumes -- Parse.for_fixes >> (fn ((a, b), c) => (c, b, a)); val _ = Outer_Syntax.command \<^command_keyword>\axiomatization\ "axiomatic constant specification" (Scan.optional Parse.vars [] -- Scan.optional (Parse.where_ |-- Parse.!!! axiomatization) ([], [], []) >> (fn (a, (b, c, d)) => Toplevel.theory (#2 o Specification.axiomatization_cmd a b c d))); val _ = Outer_Syntax.local_theory \<^command_keyword>\alias\ "name-space alias for constant" (Parse.binding -- (Parse.!!! \<^keyword>\=\ |-- Parse.name_position) >> Specification.alias_cmd); val _ = Outer_Syntax.local_theory \<^command_keyword>\type_alias\ "name-space alias for type constructor" (Parse.binding -- (Parse.!!! \<^keyword>\=\ |-- Parse.name_position) >> Specification.type_alias_cmd); in end\ subsubsection \Notation\ ML \ local val _ = Outer_Syntax.local_theory \<^command_keyword>\type_notation\ "add concrete syntax for type constructors" (Parse.syntax_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix) >> (fn (mode, args) => Specification.type_notation_cmd true mode args)); val _ = Outer_Syntax.local_theory \<^command_keyword>\no_type_notation\ "delete concrete syntax for type constructors" (Parse.syntax_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix) >> (fn (mode, args) => Specification.type_notation_cmd false mode args)); val _ = Outer_Syntax.local_theory \<^command_keyword>\notation\ "add concrete syntax for constants / fixed variables" (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix) >> (fn (mode, args) => Specification.notation_cmd true mode args)); val _ = Outer_Syntax.local_theory \<^command_keyword>\no_notation\ "delete concrete syntax for constants / fixed variables" (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix) >> (fn (mode, args) => Specification.notation_cmd false mode args)); in end\ subsubsection \Theorems\ ML \ local val long_keyword = Parse_Spec.includes >> K "" || Parse_Spec.long_statement_keyword; val long_statement = Scan.optional (Parse_Spec.opt_thm_name ":" --| Scan.ahead long_keyword) Binding.empty_atts -- Scan.optional Parse_Spec.includes [] -- Parse_Spec.long_statement >> (fn ((binding, includes), (elems, concl)) => (true, binding, includes, elems, concl)); val short_statement = Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes >> (fn ((shows, assumes), fixes) => (false, Binding.empty_atts, [], [Element.Fixes fixes, Element.Assumes assumes], Element.Shows shows)); fun theorem spec schematic descr = Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr) ((long_statement || short_statement) >> (fn (long, binding, includes, elems, concl) => ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd) long Thm.theoremK NONE (K I) binding includes elems concl))); val _ = theorem \<^command_keyword>\theorem\ false "theorem"; val _ = theorem \<^command_keyword>\lemma\ false "lemma"; val _ = theorem \<^command_keyword>\corollary\ false "corollary"; val _ = theorem \<^command_keyword>\proposition\ false "proposition"; val _ = theorem \<^command_keyword>\schematic_goal\ true "schematic goal"; in end\ ML \ local val _ = Outer_Syntax.local_theory' \<^command_keyword>\lemmas\ "define theorems" (Parse_Spec.name_facts -- Parse.for_fixes >> (fn (facts, fixes) => #2 oo Specification.theorems_cmd Thm.theoremK facts fixes)); val _ = Outer_Syntax.local_theory' \<^command_keyword>\declare\ "declare theorems" (Parse.and_list1 Parse.thms1 -- Parse.for_fixes >> (fn (facts, fixes) => #2 oo Specification.theorems_cmd "" [(Binding.empty_atts, flat facts)] fixes)); val _ = Outer_Syntax.local_theory \<^command_keyword>\named_theorems\ "declare named collection of theorems" (Parse.and_list1 (Parse.binding -- Scan.optional Parse.text "") >> fold (fn (b, descr) => snd o Named_Theorems.declare b descr)); in end\ subsubsection \Hide names\ ML \ local fun hide_names command_keyword what hide parse prep = Outer_Syntax.command command_keyword ("hide " ^ what ^ " from name space") ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 parse >> (fn (fully, args) => (Toplevel.theory (fn thy => let val ctxt = Proof_Context.init_global thy in fold (hide fully o prep ctxt) args thy end)))); val _ = hide_names \<^command_keyword>\hide_class\ "classes" Sign.hide_class Parse.class Proof_Context.read_class; val _ = hide_names \<^command_keyword>\hide_type\ "types" Sign.hide_type Parse.type_const ((#1 o dest_Type) oo Proof_Context.read_type_name {proper = true, strict = false}); val _ = hide_names \<^command_keyword>\hide_const\ "consts" Sign.hide_const Parse.const ((#1 o dest_Const) oo Proof_Context.read_const {proper = true, strict = false}); val _ = hide_names \<^command_keyword>\hide_fact\ "facts" Global_Theory.hide_fact Parse.name_position (Global_Theory.check_fact o Proof_Context.theory_of); in end\ subsection \Bundled declarations\ ML \ local val _ = Outer_Syntax.maybe_begin_local_theory \<^command_keyword>\bundle\ "define bundle of declarations" ((Parse.binding --| \<^keyword>\=\) -- Parse.thms1 -- Parse.for_fixes >> (uncurry Bundle.bundle_cmd)) (Parse.binding --| Parse.begin >> Bundle.init); val _ = Outer_Syntax.local_theory \<^command_keyword>\unbundle\ "activate declarations from bundle in local theory" (Scan.repeat1 Parse.name_position >> Bundle.unbundle_cmd); val _ = Outer_Syntax.command \<^command_keyword>\include\ "activate declarations from bundle in proof body" (Scan.repeat1 Parse.name_position >> (Toplevel.proof o Bundle.include_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\including\ "activate declarations from bundle in goal refinement" (Scan.repeat1 Parse.name_position >> (Toplevel.proof o Bundle.including_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\print_bundles\ "print bundles of declarations" (Parse.opt_bang >> (fn b => Toplevel.keep (Bundle.print_bundles b o Toplevel.context_of))); in end\ subsection \Local theory specifications\ subsubsection \Specification context\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\context\ "begin local theory context" ((Parse.name_position >> (Toplevel.begin_local_theory true o Named_Target.begin) || Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element >> (fn (incls, elems) => Toplevel.open_target (#2 o Bundle.context_cmd incls elems))) --| Parse.begin); val _ = Outer_Syntax.command \<^command_keyword>\end\ "end context" (Scan.succeed (Toplevel.exit o Toplevel.end_local_theory o Toplevel.close_target o Toplevel.end_proof (K Proof.end_notepad))); in end\ subsubsection \Locales and interpretation\ ML \ local val locale_val = Parse_Spec.locale_expression -- Scan.optional (\<^keyword>\+\ |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] || Scan.repeat1 Parse_Spec.context_element >> pair ([], []); val _ = Outer_Syntax.command \<^command_keyword>\locale\ "define named specification context" (Parse.binding -- Scan.optional (\<^keyword>\=\ |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin >> (fn ((name, (expr, elems)), begin) => Toplevel.begin_local_theory begin (Expression.add_locale_cmd name Binding.empty expr elems #> snd))); val _ = Outer_Syntax.command \<^command_keyword>\experiment\ "open private specification context" (Scan.repeat Parse_Spec.context_element --| Parse.begin >> (fn elems => Toplevel.begin_local_theory true (Experiment.experiment_cmd elems #> snd))); val _ = Outer_Syntax.command \<^command_keyword>\interpret\ "prove interpretation of locale expression in proof context" (Parse.!!! Parse_Spec.locale_expression >> (fn expr => Toplevel.proof (Interpretation.interpret_cmd expr))); val interpretation_args_with_defs = Parse.!!! Parse_Spec.locale_expression -- (Scan.optional (\<^keyword>\defines\ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- ((Parse.binding -- Parse.opt_mixfix') --| \<^keyword>\=\ -- Parse.term))) ([])); val _ = Outer_Syntax.local_theory_to_proof \<^command_keyword>\global_interpretation\ "prove interpretation of locale expression into global theory" (interpretation_args_with_defs >> (fn (expr, defs) => Interpretation.global_interpretation_cmd expr defs)); val _ = Outer_Syntax.command \<^command_keyword>\sublocale\ "prove sublocale relation between a locale and a locale expression" ((Parse.name_position --| (\<^keyword>\\\ || \<^keyword>\<\) -- interpretation_args_with_defs >> (fn (loc, (expr, defs)) => Toplevel.theory_to_proof (Interpretation.global_sublocale_cmd loc expr defs))) || interpretation_args_with_defs >> (fn (expr, defs) => Toplevel.local_theory_to_proof NONE NONE (Interpretation.sublocale_cmd expr defs))); val _ = Outer_Syntax.command \<^command_keyword>\interpretation\ "prove interpretation of locale expression in local theory or into global theory" (Parse.!!! Parse_Spec.locale_expression >> (fn expr => Toplevel.local_theory_to_proof NONE NONE (Interpretation.isar_interpretation_cmd expr))); in end\ subsubsection \Type classes\ ML \ local val class_val = Parse_Spec.class_expression -- Scan.optional (\<^keyword>\+\ |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] || Scan.repeat1 Parse_Spec.context_element >> pair []; val _ = Outer_Syntax.command \<^command_keyword>\class\ "define type class" (Parse.binding -- Scan.optional (\<^keyword>\=\ |-- class_val) ([], []) -- Parse.opt_begin >> (fn ((name, (supclasses, elems)), begin) => Toplevel.begin_local_theory begin (Class_Declaration.class_cmd name supclasses elems #> snd))); val _ = Outer_Syntax.local_theory_to_proof \<^command_keyword>\subclass\ "prove a subclass relation" (Parse.class >> Class_Declaration.subclass_cmd); val _ = Outer_Syntax.command \<^command_keyword>\instantiation\ "instantiate and prove type arity" (Parse.multi_arity --| Parse.begin >> (fn arities => Toplevel.begin_local_theory true (Class.instantiation_cmd arities))); val _ = Outer_Syntax.command \<^command_keyword>\instance\ "prove type arity or subclass relation" ((Parse.class -- ((\<^keyword>\\\ || \<^keyword>\<\) |-- Parse.!!! Parse.class) >> Class.classrel_cmd || Parse.multi_arity >> Class.instance_arity_cmd) >> Toplevel.theory_to_proof || Scan.succeed (Toplevel.local_theory_to_proof NONE NONE (Class.instantiation_instance I))); in end\ subsubsection \Arbitrary overloading\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\overloading\ "overloaded definitions" (Scan.repeat1 (Parse.name --| (\<^keyword>\==\ || \<^keyword>\\\) -- Parse.term -- Scan.optional (\<^keyword>\(\ |-- (\<^keyword>\unchecked\ >> K false) --| \<^keyword>\)\) true >> Scan.triple1) --| Parse.begin >> (fn operations => Toplevel.begin_local_theory true (Overloading.overloading_cmd operations))); in end\ subsection \Proof commands\ ML \ local val _ = Outer_Syntax.local_theory_to_proof \<^command_keyword>\notepad\ "begin proof context" (Parse.begin >> K Proof.begin_notepad); in end\ subsubsection \Statements\ ML \ local val structured_statement = Parse_Spec.statement -- Parse_Spec.cond_statement -- Parse.for_fixes >> (fn ((shows, (strict, assumes)), fixes) => (strict, fixes, assumes, shows)); val _ = Outer_Syntax.command \<^command_keyword>\have\ "state local goal" (structured_statement >> (fn (a, b, c, d) => Toplevel.proof' (fn int => Proof.have_cmd a NONE (K I) b c d int #> #2))); val _ = Outer_Syntax.command \<^command_keyword>\show\ "state local goal, to refine pending subgoals" (structured_statement >> (fn (a, b, c, d) => Toplevel.proof' (fn int => Proof.show_cmd a NONE (K I) b c d int #> #2))); val _ = Outer_Syntax.command \<^command_keyword>\hence\ "old-style alias of \"then have\"" (structured_statement >> (fn (a, b, c, d) => Toplevel.proof' (fn int => Proof.chain #> Proof.have_cmd a NONE (K I) b c d int #> #2))); val _ = Outer_Syntax.command \<^command_keyword>\thus\ "old-style alias of \"then show\"" (structured_statement >> (fn (a, b, c, d) => Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd a NONE (K I) b c d int #> #2))); in end\ subsubsection \Local facts\ ML \ local val facts = Parse.and_list1 Parse.thms1; val _ = Outer_Syntax.command \<^command_keyword>\then\ "forward chaining" (Scan.succeed (Toplevel.proof Proof.chain)); val _ = Outer_Syntax.command \<^command_keyword>\from\ "forward chaining from given facts" (facts >> (Toplevel.proof o Proof.from_thmss_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\with\ "forward chaining from given and current facts" (facts >> (Toplevel.proof o Proof.with_thmss_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\note\ "define facts" (Parse_Spec.name_facts >> (Toplevel.proof o Proof.note_thmss_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\supply\ "define facts during goal refinement (unstructured)" (Parse_Spec.name_facts >> (Toplevel.proof o Proof.supply_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\using\ "augment goal facts" (facts >> (Toplevel.proof o Proof.using_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\unfolding\ "unfold definitions in goal and facts" (facts >> (Toplevel.proof o Proof.unfolding_cmd)); in end\ subsubsection \Proof context\ ML \ local val structured_statement = Parse_Spec.statement -- Parse_Spec.if_statement' -- Parse.for_fixes >> (fn ((shows, assumes), fixes) => (fixes, assumes, shows)); val _ = Outer_Syntax.command \<^command_keyword>\fix\ "fix local variables (Skolem constants)" (Parse.vars >> (Toplevel.proof o Proof.fix_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\assume\ "assume propositions" (structured_statement >> (fn (a, b, c) => Toplevel.proof (Proof.assume_cmd a b c))); val _ = Outer_Syntax.command \<^command_keyword>\presume\ "assume propositions, to be established later" (structured_statement >> (fn (a, b, c) => Toplevel.proof (Proof.presume_cmd a b c))); val _ = Outer_Syntax.command \<^command_keyword>\define\ "local definition (non-polymorphic)" ((Parse.vars --| Parse.where_) -- Parse_Spec.statement -- Parse.for_fixes >> (fn ((a, b), c) => Toplevel.proof (Proof.define_cmd a c b))); val _ = Outer_Syntax.command \<^command_keyword>\consider\ "state cases rule" (Parse_Spec.obtains >> (Toplevel.proof' o Obtain.consider_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\obtain\ "generalized elimination" (Parse.parbinding -- Scan.optional (Parse.vars --| Parse.where_) [] -- structured_statement >> (fn ((a, b), (c, d, e)) => Toplevel.proof' (Obtain.obtain_cmd a b c d e))); val _ = Outer_Syntax.command \<^command_keyword>\guess\ "wild guessing (unstructured)" (Scan.optional Parse.vars [] >> (Toplevel.proof' o Obtain.guess_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\let\ "bind text variables" (Parse.and_list1 (Parse.and_list1 Parse.term -- (\<^keyword>\=\ |-- Parse.term)) >> (Toplevel.proof o Proof.let_bind_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\write\ "add concrete syntax for constants / fixed variables" (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix) >> (fn (mode, args) => Toplevel.proof (Proof.write_cmd mode args))); val _ = Outer_Syntax.command \<^command_keyword>\case\ "invoke local context" (Parse_Spec.opt_thm_name ":" -- (\<^keyword>\(\ |-- Parse.!!! (Parse.name_position -- Scan.repeat (Parse.maybe Parse.binding) --| \<^keyword>\)\) || Parse.name_position >> rpair []) >> (Toplevel.proof o Proof.case_cmd)); in end\ subsubsection \Proof structure\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\{\ "begin explicit proof block" (Scan.succeed (Toplevel.proof Proof.begin_block)); val _ = Outer_Syntax.command \<^command_keyword>\}\ "end explicit proof block" (Scan.succeed (Toplevel.proof Proof.end_block)); val _ = Outer_Syntax.command \<^command_keyword>\next\ "enter next proof block" (Scan.succeed (Toplevel.proof Proof.next_block)); in end\ subsubsection \End proof\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\qed\ "conclude proof" (Scan.option Method.parse >> (fn m => (Option.map Method.report m; Isar_Cmd.qed m))); val _ = Outer_Syntax.command \<^command_keyword>\by\ "terminal backward proof" (Method.parse -- Scan.option Method.parse >> (fn (m1, m2) => (Method.report m1; Option.map Method.report m2; Isar_Cmd.terminal_proof (m1, m2)))); val _ = Outer_Syntax.command \<^command_keyword>\..\ "default proof" (Scan.succeed Isar_Cmd.default_proof); val _ = Outer_Syntax.command \<^command_keyword>\.\ "immediate proof" (Scan.succeed Isar_Cmd.immediate_proof); val _ = Outer_Syntax.command \<^command_keyword>\done\ "done proof" (Scan.succeed Isar_Cmd.done_proof); val _ = Outer_Syntax.command \<^command_keyword>\sorry\ "skip proof (quick-and-dirty mode only!)" (Scan.succeed Isar_Cmd.skip_proof); val _ = Outer_Syntax.command \<^command_keyword>\\\ "dummy proof (quick-and-dirty mode only!)" (Scan.succeed Isar_Cmd.skip_proof); val _ = Outer_Syntax.command \<^command_keyword>\oops\ "forget proof" (Scan.succeed Toplevel.forget_proof); in end\ subsubsection \Proof steps\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\defer\ "shuffle internal proof state" (Scan.optional Parse.nat 1 >> (Toplevel.proof o Proof.defer)); val _ = Outer_Syntax.command \<^command_keyword>\prefer\ "shuffle internal proof state" (Parse.nat >> (Toplevel.proof o Proof.prefer)); val _ = Outer_Syntax.command \<^command_keyword>\apply\ "initial goal refinement step (unstructured)" (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply m)))); val _ = Outer_Syntax.command \<^command_keyword>\apply_end\ "terminal goal refinement step (unstructured)" (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_end m)))); val _ = Outer_Syntax.command \<^command_keyword>\proof\ "backward proof step" (Scan.option Method.parse >> (fn m => (Option.map Method.report m; Toplevel.proof (fn state => let val state' = state |> Proof.proof m |> Seq.the_result ""; val _ = Output.information (Proof_Context.print_cases_proof (Proof.context_of state) (Proof.context_of state')); in state' end)))) in end\ subsubsection \Subgoal focus\ ML \ local val opt_fact_binding = Scan.optional (Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty) Binding.empty_atts; val for_params = Scan.optional (\<^keyword>\for\ |-- Parse.!!! ((Scan.option Parse.dots >> is_some) -- (Scan.repeat1 (Parse.maybe_position Parse.name_position)))) (false, []); val _ = Outer_Syntax.command \<^command_keyword>\subgoal\ "focus on first subgoal within backward refinement" (opt_fact_binding -- (Scan.option (\<^keyword>\premises\ |-- Parse.!!! opt_fact_binding)) -- for_params >> (fn ((a, b), c) => Toplevel.proofs (Seq.make_results o Seq.single o #2 o Subgoal.subgoal_cmd a b c))); in end\ subsubsection \Calculation\ ML \ local val calculation_args = Scan.option (\<^keyword>\(\ |-- Parse.!!! ((Parse.thms1 --| \<^keyword>\)\))); val _ = Outer_Syntax.command \<^command_keyword>\also\ "combine calculation and current facts" (calculation_args >> (Toplevel.proofs' o Calculation.also_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\finally\ "combine calculation and current facts, exhibit result" (calculation_args >> (Toplevel.proofs' o Calculation.finally_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\moreover\ "augment calculation by current facts" (Scan.succeed (Toplevel.proof' Calculation.moreover)); val _ = Outer_Syntax.command \<^command_keyword>\ultimately\ "augment calculation by current facts, exhibit result" (Scan.succeed (Toplevel.proof' Calculation.ultimately)); val _ = Outer_Syntax.command \<^command_keyword>\print_trans_rules\ "print transitivity rules" (Scan.succeed (Toplevel.keep (Calculation.print_rules o Toplevel.context_of))); in end\ subsubsection \Proof navigation\ ML \ local fun report_back () = Output.report [Markup.markup (Markup.bad ()) "Explicit backtracking"]; val _ = Outer_Syntax.command \<^command_keyword>\back\ "explicit backtracking of proof command" (Scan.succeed (Toplevel.actual_proof (fn prf => (report_back (); Proof_Node.back prf)) o Toplevel.skip_proof report_back)); in end\ subsection \Diagnostic commands (for interactive mode only)\ ML \ local val opt_modes = Scan.optional (\<^keyword>\(\ |-- Parse.!!! (Scan.repeat1 Parse.name --| \<^keyword>\)\)) []; val _ = Outer_Syntax.command \<^command_keyword>\help\ "retrieve outer syntax commands according to name patterns" (Scan.repeat Parse.name >> (fn pats => Toplevel.keep (fn st => Outer_Syntax.help (Toplevel.theory_of st) pats))); val _ = Outer_Syntax.command \<^command_keyword>\print_commands\ "print outer syntax commands" (Scan.succeed (Toplevel.keep (Outer_Syntax.print_commands o Toplevel.theory_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_options\ "print configuration options" (Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_options b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_context\ "print context of local theory target" (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Toplevel.pretty_context))); val _ = Outer_Syntax.command \<^command_keyword>\print_theory\ "print logical theory contents" (Parse.opt_bang >> (fn b => Toplevel.keep (Pretty.writeln o Proof_Display.pretty_theory b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_definitions\ "print dependencies of definitional theory content" (Parse.opt_bang >> (fn b => Toplevel.keep (Pretty.writeln o Proof_Display.pretty_definitions b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_syntax\ "print inner syntax of context" (Scan.succeed (Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_defn_rules\ "print definitional rewrite rules of context" (Scan.succeed (Toplevel.keep (Local_Defs.print_rules o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_abbrevs\ "print constant abbreviations of context" (Parse.opt_bang >> (fn b => Toplevel.keep (Proof_Context.print_abbrevs b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_theorems\ "print theorems of local theory or proof context" (Parse.opt_bang >> (fn b => Toplevel.keep (Pretty.writeln o Pretty.chunks o Isar_Cmd.pretty_theorems b))); val _ = Outer_Syntax.command \<^command_keyword>\print_locales\ "print locales of this theory" (Parse.opt_bang >> (fn verbose => Toplevel.keep (fn state => let val thy = Toplevel.theory_of state in Pretty.writeln (Locale.pretty_locales thy verbose) end))); val _ = Outer_Syntax.command \<^command_keyword>\print_classes\ "print classes of this theory" (Scan.succeed (Toplevel.keep (Class.print_classes o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_locale\ "print locale of this theory" (Parse.opt_bang -- Parse.name_position >> (fn (show_facts, raw_name) => Toplevel.keep (fn state => let val thy = Toplevel.theory_of state; val name = Locale.check thy raw_name; in Pretty.writeln (Locale.pretty_locale thy show_facts name) end))); val _ = Outer_Syntax.command \<^command_keyword>\print_interps\ "print interpretations of locale for this theory or proof context" (Parse.name_position >> (fn raw_name => Toplevel.keep (fn state => let val ctxt = Toplevel.context_of state; val thy = Toplevel.theory_of state; val name = Locale.check thy raw_name; in Pretty.writeln (Locale.pretty_registrations ctxt name) end))); val _ = Outer_Syntax.command \<^command_keyword>\print_dependencies\ "print dependencies of locale expression" (Parse.opt_bang -- Parse_Spec.locale_expression >> (fn (clean, expr) => Toplevel.keep (fn state => Pretty.writeln (Expression.pretty_dependencies (Toplevel.context_of state) clean expr)))); val _ = Outer_Syntax.command \<^command_keyword>\print_attributes\ "print attributes of this theory" (Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_attributes b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_simpset\ "print context of Simplifier" (Parse.opt_bang >> (fn b => Toplevel.keep (Pretty.writeln o Simplifier.pretty_simpset b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_rules\ "print intro/elim rules" (Scan.succeed (Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_methods\ "print methods of this theory" (Parse.opt_bang >> (fn b => Toplevel.keep (Method.print_methods b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_antiquotations\ "print document antiquotations" (Parse.opt_bang >> (fn b => Toplevel.keep (Document_Antiquotation.print_antiquotations b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_ML_antiquotations\ "print ML antiquotations" (Parse.opt_bang >> (fn b => Toplevel.keep (ML_Context.print_antiquotations b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\locale_deps\ "visualize locale dependencies" (Scan.succeed (Toplevel.keep (Toplevel.theory_of #> (fn thy => Locale.pretty_locale_deps thy |> map (fn {name, parents, body} => ((name, Graph_Display.content_node (Locale.extern thy name) [body]), parents)) |> Graph_Display.display_graph_old)))); val _ = Outer_Syntax.command \<^command_keyword>\print_term_bindings\ "print term bindings of proof context" (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_facts\ "print facts of proof context" (Parse.opt_bang >> (fn b => Toplevel.keep (Proof_Context.print_local_facts b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_cases\ "print cases of proof context" (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_cases o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_statement\ "print theorems as long statements" (opt_modes -- Parse.thms1 >> Isar_Cmd.print_stmts); val _ = Outer_Syntax.command \<^command_keyword>\thm\ "print theorems" (opt_modes -- Parse.thms1 >> Isar_Cmd.print_thms); val _ = Outer_Syntax.command \<^command_keyword>\prf\ "print proof terms of theorems" (opt_modes -- Scan.option Parse.thms1 >> Isar_Cmd.print_prfs false); val _ = Outer_Syntax.command \<^command_keyword>\full_prf\ "print full proof terms of theorems" (opt_modes -- Scan.option Parse.thms1 >> Isar_Cmd.print_prfs true); val _ = Outer_Syntax.command \<^command_keyword>\prop\ "read and print proposition" (opt_modes -- Parse.term >> Isar_Cmd.print_prop); val _ = Outer_Syntax.command \<^command_keyword>\term\ "read and print term" (opt_modes -- Parse.term >> Isar_Cmd.print_term); val _ = Outer_Syntax.command \<^command_keyword>\typ\ "read and print type" (opt_modes -- (Parse.typ -- Scan.option (\<^keyword>\::\ |-- Parse.!!! Parse.sort)) >> Isar_Cmd.print_type); val _ = Outer_Syntax.command \<^command_keyword>\print_codesetup\ "print code generator setup" (Scan.succeed (Toplevel.keep (Code.print_codesetup o Toplevel.theory_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_state\ "print current proof state (if present)" (opt_modes >> (fn modes => Toplevel.keep (Print_Mode.with_modes modes (Output.state o Toplevel.string_of_state)))); val _ = Outer_Syntax.command \<^command_keyword>\welcome\ "print welcome message" (Scan.succeed (Toplevel.keep (fn _ => writeln (Session.welcome ())))); in end\ subsection \Dependencies\ ML \ local val theory_bounds = Parse.theory_name >> single || (\<^keyword>\(\ |-- Parse.enum "|" Parse.theory_name --| \<^keyword>\)\); val _ = Outer_Syntax.command \<^command_keyword>\thy_deps\ "visualize theory dependencies" (Scan.option theory_bounds -- Scan.option theory_bounds >> (fn args => Toplevel.keep (fn st => Thy_Deps.thy_deps_cmd (Toplevel.context_of st) args))); val class_bounds = Parse.sort >> single || (\<^keyword>\(\ |-- Parse.enum "|" Parse.sort --| \<^keyword>\)\); val _ = Outer_Syntax.command \<^command_keyword>\class_deps\ "visualize class dependencies" (Scan.option class_bounds -- Scan.option class_bounds >> (fn args => Toplevel.keep (fn st => Class_Deps.class_deps_cmd (Toplevel.context_of st) args))); val _ = Outer_Syntax.command \<^command_keyword>\thm_deps\ "visualize theorem dependencies" (Parse.thms1 >> (fn args => Toplevel.keep (fn st => Thm_Deps.thm_deps (Toplevel.theory_of st) (Attrib.eval_thms (Toplevel.context_of st) args)))); val thy_names = Scan.repeat1 (Scan.unless Parse.minus Parse.theory_name); val _ = Outer_Syntax.command \<^command_keyword>\unused_thms\ "find unused theorems" (Scan.option ((thy_names --| Parse.minus) -- Scan.option thy_names) >> (fn opt_range => Toplevel.keep (fn st => let val thy = Toplevel.theory_of st; val ctxt = Toplevel.context_of st; fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]); val check = Theory.check {long = false} ctxt; in Thm_Deps.unused_thms (case opt_range of NONE => (Theory.parents_of thy, [thy]) | SOME (xs, NONE) => (map check xs, [thy]) | SOME (xs, SOME ys) => (map check xs, map check ys)) |> map pretty_thm |> Pretty.writeln_chunks end))); in end\ subsubsection \Find consts and theorems\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\find_consts\ "find constants by name / type patterns" (Find_Consts.query_parser >> (fn spec => Toplevel.keep (fn st => Pretty.writeln (Find_Consts.pretty_consts (Toplevel.context_of st) spec)))); val options = Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.option Parse.nat -- Scan.optional (Parse.reserved "with_dups" >> K false) true --| Parse.$$$ ")")) (NONE, true); val _ = Outer_Syntax.command \<^command_keyword>\find_theorems\ "find theorems meeting specified criteria" (options -- Find_Theorems.query_parser >> (fn ((opt_lim, rem_dups), spec) => Toplevel.keep (fn st => Pretty.writeln (Find_Theorems.pretty_theorems (Find_Theorems.proof_state st) opt_lim rem_dups spec)))); in end\ subsection \Code generation\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\code_datatype\ "define set of code datatype constructors" (Scan.repeat1 Parse.term >> (Toplevel.theory o Code.declare_datatype_cmd)); in end\ subsection \Extraction of programs from proofs\ ML \ local val parse_vars = Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.name --| Parse.$$$ ")") []; val _ = Outer_Syntax.command \<^command_keyword>\realizers\ "specify realizers for primitive axioms / theorems, together with correctness proof" (Scan.repeat1 (Parse.name -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >> (fn xs => Toplevel.theory (fn thy => Extraction.add_realizers (map (fn (((a, vs), s1), s2) => (Global_Theory.get_thm thy a, (vs, s1, s2))) xs) thy))); val _ = Outer_Syntax.command \<^command_keyword>\realizability\ "add equations characterizing realizability" (Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_realizes_eqns)); val _ = Outer_Syntax.command \<^command_keyword>\extract_type\ "add equations characterizing type of extracted program" (Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_typeof_eqns)); val _ = Outer_Syntax.command \<^command_keyword>\extract\ "extract terms from proofs" (Scan.repeat1 (Parse.name -- parse_vars) >> (fn xs => Toplevel.theory (fn thy => Extraction.extract (map (apfst (Global_Theory.get_thm thy)) xs) thy))); in end\ section \Auxiliary lemmas\ subsection \Meta-level connectives in assumptions\ lemma meta_mp: assumes "PROP P \ PROP Q" and "PROP P" shows "PROP Q" by (rule \PROP P \ PROP Q\ [OF \PROP P\]) lemmas meta_impE = meta_mp [elim_format] lemma meta_spec: assumes "\x. PROP P x" shows "PROP P x" by (rule \\x. PROP P x\) lemmas meta_allE = meta_spec [elim_format] lemma swap_params: "(\x y. PROP P x y) \ (\y x. PROP P x y)" .. subsection \Meta-level conjunction\ lemma all_conjunction: "(\x. PROP A x &&& PROP B x) \ ((\x. PROP A x) &&& (\x. PROP B x))" proof assume conj: "\x. PROP A x &&& PROP B x" show "(\x. PROP A x) &&& (\x. PROP B x)" proof - fix x from conj show "PROP A x" by (rule conjunctionD1) from conj show "PROP B x" by (rule conjunctionD2) qed next assume conj: "(\x. PROP A x) &&& (\x. PROP B x)" fix x show "PROP A x &&& PROP B x" proof - show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format]) show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format]) qed qed lemma imp_conjunction: "(PROP A \ PROP B &&& PROP C) \ ((PROP A \ PROP B) &&& (PROP A \ PROP C))" proof assume conj: "PROP A \ PROP B &&& PROP C" show "(PROP A \ PROP B) &&& (PROP A \ PROP C)" proof - assume "PROP A" from conj [OF \PROP A\] show "PROP B" by (rule conjunctionD1) from conj [OF \PROP A\] show "PROP C" by (rule conjunctionD2) qed next assume conj: "(PROP A \ PROP B) &&& (PROP A \ PROP C)" assume "PROP A" show "PROP B &&& PROP C" proof - from \PROP A\ show "PROP B" by (rule conj [THEN conjunctionD1]) from \PROP A\ show "PROP C" by (rule conj [THEN conjunctionD2]) qed qed lemma conjunction_imp: "(PROP A &&& PROP B \ PROP C) \ (PROP A \ PROP B \ PROP C)" proof assume r: "PROP A &&& PROP B \ PROP C" assume ab: "PROP A" "PROP B" show "PROP C" proof (rule r) from ab show "PROP A &&& PROP B" . qed next assume r: "PROP A \ PROP B \ PROP C" assume conj: "PROP A &&& PROP B" show "PROP C" proof (rule r) from conj show "PROP A" by (rule conjunctionD1) from conj show "PROP B" by (rule conjunctionD2) qed qed declare [[ML_write_global = false]] end diff --git a/src/Pure/Syntax/lexicon.ML b/src/Pure/Syntax/lexicon.ML --- a/src/Pure/Syntax/lexicon.ML +++ b/src/Pure/Syntax/lexicon.ML @@ -1,487 +1,487 @@ (* Title: Pure/Syntax/lexicon.ML Author: Tobias Nipkow and Markus Wenzel, TU Muenchen Lexer for the inner Isabelle syntax (terms and types). *) signature LEXICON = sig structure Syntax: sig val const: string -> term val free: string -> term val var: indexname -> term end val scan_id: Symbol_Pos.T list scanner val scan_longid: Symbol_Pos.T list scanner val scan_tid: Symbol_Pos.T list scanner val scan_hex: Symbol_Pos.T list scanner val scan_bin: Symbol_Pos.T list scanner val scan_var: Symbol_Pos.T list scanner val scan_tvar: Symbol_Pos.T list scanner val is_tid: string -> bool datatype token_kind = Literal | Ident | Long_Ident | Var | Type_Ident | Type_Var | Num | Float | Str | String | Cartouche | Space | Comment of Comment.kind | Dummy | EOF eqtype token val kind_of_token: token -> token_kind val str_of_token: token -> string val pos_of_token: token -> Position.T val end_pos_of_token: token -> Position.T val is_proper: token -> bool val dummy: token val literal: string -> token val is_literal: token -> bool val tokens_match_ord: token * token -> order val mk_eof: Position.T -> token val eof: token val is_eof: token -> bool val stopper: token Scan.stopper val terminals: string list val is_terminal: string -> bool val get_terminal: string -> token option val literal_markup: string -> Markup.T val report_of_token: token -> Position.report val reported_token_range: Proof.context -> token -> string val valued_token: token -> bool val implode_string: Symbol.symbol list -> string val explode_string: string * Position.T -> Symbol_Pos.T list val implode_str: Symbol.symbol list -> string val explode_str: string * Position.T -> Symbol_Pos.T list val tokenize: Scan.lexicon -> bool -> Symbol_Pos.T list -> token list val read_indexname: string -> indexname val read_var: string -> term val read_variable: string -> indexname option val read_nat: string -> int option val read_int: string -> int option val read_num: string -> {radix: int, leading_zeros: int, value: int} val read_float: string -> {mant: int, exp: int} val mark_class: string -> string val unmark_class: string -> string val mark_type: string -> string val unmark_type: string -> string val mark_const: string -> string val unmark_const: string -> string val mark_fixed: string -> string val unmark_fixed: string -> string val unmark: {case_class: string -> 'a, case_type: string -> 'a, case_const: string -> 'a, case_fixed: string -> 'a, case_default: string -> 'a} -> string -> 'a val is_marked: string -> bool val dummy_type: term val fun_type: term end; structure Lexicon: LEXICON = struct (** syntactic terms **) structure Syntax = struct fun const c = Const (c, dummyT); fun free x = Free (x, dummyT); fun var xi = Var (xi, dummyT); end; (** basic scanners **) open Basic_Symbol_Pos; val err_prefix = "Inner lexical error: "; fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg); val scan_id = Symbol_Pos.scan_ident; val scan_longid = scan_id @@@ Scan.repeats1 ($$$ "." @@@ scan_id); val scan_tid = $$$ "'" @@@ scan_id; val scan_hex = $$$ "0" @@@ $$$ "x" @@@ Scan.many1 (Symbol.is_ascii_hex o Symbol_Pos.symbol); val scan_bin = $$$ "0" @@@ $$$ "b" @@@ Scan.many1 (fn (s, _) => s = "0" orelse s = "1"); val scan_num = scan_hex || scan_bin || Symbol_Pos.scan_nat; val scan_id_nat = scan_id @@@ Scan.optional ($$$ "." @@@ Symbol_Pos.scan_nat) []; val scan_var = $$$ "?" @@@ scan_id_nat; val scan_tvar = $$$ "?" @@@ $$$ "'" @@@ scan_id_nat; fun is_tid s = (case try (unprefix "'") s of SOME s' => Symbol_Pos.is_identifier s' | NONE => false); (** tokens **) (* datatype token_kind *) datatype token_kind = Literal | Ident | Long_Ident | Var | Type_Ident | Type_Var | Num | Float | Str | String | Cartouche | Space | Comment of Comment.kind | Dummy | EOF; val token_kinds = Vector.fromList [Literal, Ident, Long_Ident, Var, Type_Ident, Type_Var, Num, Float, Str, String, Cartouche, Space, Comment Comment.Comment, Comment Comment.Cancel, Comment Comment.Latex, Dummy, EOF]; fun token_kind i = Vector.sub (token_kinds, i); fun token_kind_index k = #1 (the (Vector.findi (fn (_, k') => k = k') token_kinds)); (* datatype token *) datatype token = Token of int * string * Position.range; fun index_of_token (Token (i, _, _)) = i; val kind_of_token = index_of_token #> token_kind; fun str_of_token (Token (_, s, _)) = s; fun pos_of_token (Token (_, _, (pos, _))) = pos; fun end_pos_of_token (Token (_, _, (_, end_pos))) = end_pos; val is_proper = kind_of_token #> (fn Space => false | Comment _ => false | _ => true); val dummy = Token (token_kind_index Dummy, "", Position.no_range); (* literals *) val literal_index = token_kind_index Literal; fun literal s = Token (literal_index, s, Position.no_range); fun is_literal tok = index_of_token tok = literal_index; fun tokens_match_ord toks = let val is = apply2 index_of_token toks in (case int_ord is of EQUAL => if #1 is = literal_index then fast_string_ord (apply2 str_of_token toks) else EQUAL | ord => ord) end; (* stopper *) val eof_index = token_kind_index EOF; fun mk_eof pos = Token (eof_index, "", (pos, Position.none)); val eof = mk_eof Position.none; fun is_eof tok = index_of_token tok = eof_index; val stopper = Scan.stopper (K eof) is_eof; (* terminal symbols *) val terminal_symbols = [("id", Ident), ("longid", Long_Ident), ("var", Var), ("tid", Type_Ident), ("tvar", Type_Var), ("num_token", Num), ("float_token", Float), ("str_token", Str), ("string_token", String), ("cartouche", Cartouche)] |> map (apsnd token_kind_index) |> Symtab.make; val terminals = Symtab.keys terminal_symbols; val is_terminal = Symtab.defined terminal_symbols; fun get_terminal s = (case Symtab.lookup terminal_symbols s of SOME i => SOME (Token (i, s, Position.no_range)) | NONE => NONE); (* markup *) fun literal_markup s = if Symbol.is_ascii_identifier s orelse exists Symbol.is_letter (Symbol.explode s) then Markup.literal else Markup.delimiter; val token_kind_markup = fn Type_Ident => Markup.tfree | Type_Var => Markup.tvar | Num => Markup.numeral | Float => Markup.numeral | Str => Markup.inner_string | String => Markup.inner_string | Cartouche => Markup.inner_cartouche | Comment _ => Markup.comment1 | _ => Markup.empty; fun report_of_token tok = let val markup = if is_literal tok then literal_markup (str_of_token tok) else token_kind_markup (kind_of_token tok); in (pos_of_token tok, markup) end; fun reported_token_range ctxt tok = if is_proper tok then Context_Position.reported_text ctxt (pos_of_token tok) Markup.token_range "" else ""; (* valued_token *) fun valued_token tok = not (is_literal tok orelse is_eof tok); (** string literals **) fun explode_literal scan_body (str, pos) = (case Scan.read Symbol_Pos.stopper scan_body (Symbol_Pos.explode (str, pos)) of SOME ss => ss | _ => error (err_prefix ^ "malformed string literal " ^ quote str ^ Position.here pos)); (* string *) val scan_string = Scan.trace (Symbol_Pos.scan_string_qq err_prefix) >> #2; val scan_string_body = Symbol_Pos.scan_string_qq err_prefix >> (#1 o #2); fun implode_string ss = quote (implode (map (fn "\"" => "\\\"" | s => s) ss)); val explode_string = explode_literal scan_string_body; (* str *) val scan_chr = $$ "\\" |-- $$$ "'" || Scan.one ((fn s => s <> "\\" andalso s <> "'" andalso Symbol.not_eof s) o Symbol_Pos.symbol) >> single || $$$ "'" --| Scan.ahead (~$$ "'"); val scan_str = Scan.ahead ($$ "'" -- $$ "'") |-- !!! "unclosed string literal" ($$$ "'" @@@ $$$ "'" @@@ Scan.repeats scan_chr @@@ $$$ "'" @@@ $$$ "'"); val scan_str_body = Scan.ahead ($$ "'" |-- $$ "'") |-- !!! "unclosed string literal" ($$ "'" |-- $$ "'" |-- Scan.repeats scan_chr --| $$ "'" --| $$ "'"); fun implode_str ss = enclose "''" "''" (implode (map (fn "'" => "\\'" | s => s) ss)); val explode_str = explode_literal scan_str_body; (** tokenize **) val token_leq = op <= o apply2 str_of_token; fun token kind = let val i = token_kind_index kind in fn ss => Token (i, Symbol_Pos.content ss, Symbol_Pos.range ss) end; fun tokenize lex xids syms = let val scan_xid = (if xids then $$$ "_" @@@ scan_id || scan_id else scan_id) || $$$ "_" @@@ $$$ "_"; val scan_val = scan_tvar >> token Type_Var || scan_var >> token Var || scan_tid >> token Type_Ident || Symbol_Pos.scan_float >> token Float || scan_num >> token Num || scan_longid >> token Long_Ident || scan_xid >> token Ident; val scan_lit = Scan.literal lex >> token Literal; val scan = Symbol_Pos.scan_cartouche err_prefix >> token Cartouche || - Comment.scan >> (fn (kind, ss) => token (Comment kind) ss) || + Comment.scan_inner >> (fn (kind, ss) => token (Comment kind) ss) || Scan.max token_leq scan_lit scan_val || scan_string >> token String || scan_str >> token Str || Scan.many1 (Symbol.is_blank o Symbol_Pos.symbol) >> token Space; in (case Scan.error (Scan.finite Symbol_Pos.stopper (Scan.repeat scan)) syms of (toks, []) => toks | (_, ss) => error ("Inner lexical error" ^ Position.here (#1 (Symbol_Pos.range ss)) ^ Markup.markup Markup.no_report ("\nat " ^ quote (Symbol_Pos.content ss)))) end; (** scan variables **) (* scan_indexname *) local val scan_vname = let fun nat n [] = n | nat n (c :: cs) = nat (n * 10 + (ord c - Char.ord #"0")) cs; fun idxname cs ds = (implode (rev cs), nat 0 ds); fun chop_idx [] ds = idxname [] ds | chop_idx (cs as (_ :: "\<^sub>" :: _)) ds = idxname cs ds | chop_idx (c :: cs) ds = if Symbol.is_digit c then chop_idx cs (c :: ds) else idxname (c :: cs) ds; val scan = (scan_id >> map Symbol_Pos.symbol) -- Scan.optional ($$ "." |-- Symbol_Pos.scan_nat >> (nat 0 o map Symbol_Pos.symbol)) ~1; in scan >> (fn (cs, ~1) => chop_idx (rev cs) [] | (cs, i) => (implode cs, i)) end; in val scan_indexname = $$ "'" |-- scan_vname >> (fn (x, i) => ("'" ^ x, i)) || scan_vname; end; (* indexname *) fun read_indexname s = (case Scan.read Symbol_Pos.stopper scan_indexname (Symbol_Pos.explode0 s) of SOME xi => xi | _ => error ("Lexical error in variable name: " ^ quote s)); (* read_var *) fun read_var str = let val scan = $$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol_Pos.is_eof) >> Syntax.var || Scan.many (Symbol.not_eof o Symbol_Pos.symbol) >> (Syntax.free o implode o map Symbol_Pos.symbol); in the (Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode0 str)) end; (* read_variable *) fun read_variable str = let val scan = $$ "?" |-- scan_indexname || scan_indexname in Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode0 str) end; (* read numbers *) local fun nat cs = Option.map (#1 o Library.read_int o map Symbol_Pos.symbol) (Scan.read Symbol_Pos.stopper Symbol_Pos.scan_nat cs); in fun read_nat s = nat (Symbol_Pos.explode0 s); fun read_int s = (case Symbol_Pos.explode0 s of ("-", _) :: cs => Option.map ~ (nat cs) | cs => nat cs); end; (* read_num: hex/bin/decimal *) local val ten = Char.ord #"0" + 10; val a = Char.ord #"a"; val A = Char.ord #"A"; val _ = a > A orelse raise Fail "Bad ASCII"; fun remap_hex c = let val x = ord c in if x >= a then chr (x - a + ten) else if x >= A then chr (x - A + ten) else c end; fun leading_zeros ["0"] = 0 | leading_zeros ("0" :: cs) = 1 + leading_zeros cs | leading_zeros _ = 0; in fun read_num str = let val (radix, digs) = (case Symbol.explode str of "0" :: "x" :: cs => (16, map remap_hex cs) | "0" :: "b" :: cs => (2, cs) | cs => (10, cs)); in {radix = radix, leading_zeros = leading_zeros digs, value = #1 (Library.read_radix_int radix digs)} end; end; fun read_float str = let val cs = Symbol.explode str; val (intpart, fracpart) = (case chop_prefix Symbol.is_digit cs of (intpart, "." :: fracpart) => (intpart, fracpart) | _ => raise Fail "read_float"); in {mant = #1 (Library.read_int (intpart @ fracpart)), exp = length fracpart} end; (* marked logical entities *) fun marker s = (prefix s, unprefix s); val (mark_class, unmark_class) = marker "\<^class>"; val (mark_type, unmark_type) = marker "\<^type>"; val (mark_const, unmark_const) = marker "\<^const>"; val (mark_fixed, unmark_fixed) = marker "\<^fixed>"; fun unmark {case_class, case_type, case_const, case_fixed, case_default} s = (case try unmark_class s of SOME c => case_class c | NONE => (case try unmark_type s of SOME c => case_type c | NONE => (case try unmark_const s of SOME c => case_const c | NONE => (case try unmark_fixed s of SOME c => case_fixed c | NONE => case_default s)))); val is_marked = unmark {case_class = K true, case_type = K true, case_const = K true, case_fixed = K true, case_default = K false}; val dummy_type = Syntax.const (mark_type "dummy"); val fun_type = Syntax.const (mark_type "fun"); (* toplevel pretty printing *) val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Pretty.str_list "{" "}" o map quote o Scan.dest_lexicon); end; diff --git a/src/Pure/Thy/document_marker.ML b/src/Pure/Thy/document_marker.ML --- a/src/Pure/Thy/document_marker.ML +++ b/src/Pure/Thy/document_marker.ML @@ -1,80 +1,84 @@ (* Title: Pure/Thy/document_marker.ML Author: Makarius Document markers: declarations on the presentation context. *) signature DOCUMENT_MARKER = sig type marker = Proof.context -> Proof.context val setup: binding -> 'a context_parser -> ('a -> marker) -> theory -> theory val setup0: binding -> 'a parser -> ('a -> marker) -> theory -> theory val evaluate: Input.source -> marker + val legacy_tag: string -> Input.source end; structure Document_Marker: DOCUMENT_MARKER = struct (* theory data *) type marker = Proof.context -> Proof.context; structure Markers = Theory_Data ( type T = (Token.src -> Proof.context -> Proof.context) Name_Space.table; val empty : T = Name_Space.empty_table "document_marker"; val extend = I; val merge = Name_Space.merge_tables; ); val get_markers = Markers.get o Proof_Context.theory_of; fun check ctxt = Name_Space.check (Context.Proof ctxt) (get_markers ctxt); fun setup name scan body thy = let fun marker src ctxt = let val (x, ctxt') = Token.syntax scan src ctxt in body x ctxt' end; in thy |> Markers.map (Name_Space.define (Context.Theory thy) true (name, marker) #> #2) end; fun setup0 name scan = setup name (Scan.lift scan); (* evaluate inner syntax *) val parse_marker = Parse.token Parse.liberal_name ::: Parse.!!! Parse.args; fun evaluate input ctxt = let - val pos = Input.pos_of input; - val _ = Context_Position.report ctxt pos Markup.language_document_marker; - - val syms = Input.source_explode input; + val body = + Input.source_explode input + |> drop_prefix (fn (s, _) => s = Symbol.marker) + |> Symbol_Pos.cartouche_content; val markers = - (case Token.read_body (Thy_Header.get_keywords' ctxt) (Parse.list parse_marker) syms of + (case Token.read_body (Thy_Header.get_keywords' ctxt) (Parse.list parse_marker) body of SOME res => res - | NONE => error ("Bad input" ^ Position.here pos)); + | NONE => error ("Bad input" ^ Position.here (Input.pos_of input))); in fold (fn src => #2 (check ctxt (Token.name_of_src src)) src) markers ctxt end; (* concrete markers *) fun meta_data markup arg ctxt = (Context_Position.report_text ctxt (Position.thread_data ()) markup arg; ctxt); val _ = Theory.setup (setup0 (Binding.make ("tag", \<^here>)) Parse.name Document_Source.update_tags #> setup0 (Binding.make ("title", \<^here>)) Parse.embedded (meta_data Markup.meta_title) #> setup0 (Binding.make ("creator", \<^here>)) Parse.embedded (meta_data Markup.meta_creator) #> setup0 (Binding.make ("contributor", \<^here>)) Parse.embedded (meta_data Markup.meta_contributor) #> setup0 (Binding.make ("date", \<^here>)) Parse.embedded (meta_data Markup.meta_date) #> setup0 (Binding.make ("description", \<^here>)) (Parse.input Parse.embedded) (fn source => fn ctxt => let val (arg, pos) = Input.source_content source; val _ = Context_Position.report ctxt pos Markup.words; in meta_data Markup.meta_description arg ctxt end)); +fun legacy_tag name = + Input.string (cartouche ("tag " ^ Symbol_Pos.quote_string_qq name)); + end; diff --git a/src/Pure/Thy/document_source.ML b/src/Pure/Thy/document_source.ML --- a/src/Pure/Thy/document_source.ML +++ b/src/Pure/Thy/document_source.ML @@ -1,74 +1,69 @@ (* Title: Pure/Thy/document_source.ML Author: Makarius Document source for presentation. *) signature DOCUMENT_SOURCE = sig val is_white: Token.T -> bool val is_black: Token.T -> bool val is_white_comment: Token.T -> bool val is_black_comment: Token.T -> bool val is_improper: Token.T -> bool val improper: Token.T list parser val improper_end: Token.T list parser val blank_end: Token.T list parser val get_tags: Proof.context -> string list val update_tags: string -> Proof.context -> Proof.context val tags: string list parser - val annotation: Input.source list parser + val annotation: unit parser end; structure Document_Source: DOCUMENT_SOURCE = struct (* white space and comments *) (*NB: arranging white space around command spans is a black art*) val is_white = Token.is_space orf Token.is_informal_comment; val is_black = not o is_white; val is_white_comment = Token.is_informal_comment; val is_black_comment = Token.is_formal_comment; val space_proper = Scan.one Token.is_blank -- Scan.many is_white_comment -- Scan.one is_black; val is_improper = not o (is_black orf Token.is_begin_ignore orf Token.is_end_ignore); val improper = Scan.many is_improper; val improper_end = Scan.repeat (Scan.unless space_proper (Scan.one is_improper)); val blank_end = Scan.repeat (Scan.unless space_proper (Scan.one Token.is_blank)); (* syntactic tags (old-style) *) structure Tags = Proof_Data ( type T = string list; fun init _ = []; ); val get_tags = Tags.get; val update_tags = Tags.map o update (op =); val tag_name = Parse.group (fn () => "document tag name") (Parse.short_ident || Parse.string); val tag = (improper -- Parse.$$$ "%" -- improper) |-- Parse.!!! (tag_name --| blank_end); val tags = Scan.repeat tag; (* semantic markers (operation on presentation context) *) -val marker = - (improper -- Parse.$$$ "\" -- improper) |-- - Parse.!!! (Parse.group (fn () => "document marker") (Parse.input Parse.embedded) --| blank_end); +val marker = improper |-- Parse.document_marker --| blank_end; -val tag_marker = (*emulation of old-style tags*) - tag >> (fn name => Input.string ("tag " ^ Symbol_Pos.quote_string_qq name)); - -val annotation = Scan.repeat (marker || tag_marker); +val annotation = Scan.repeat (tag >> K () || marker >> K ()) >> K (); end; diff --git a/src/Pure/Thy/thy_header.ML b/src/Pure/Thy/thy_header.ML --- a/src/Pure/Thy/thy_header.ML +++ b/src/Pure/Thy/thy_header.ML @@ -1,212 +1,212 @@ (* Title: Pure/Thy/thy_header.ML Author: Makarius Static theory header information. *) signature THY_HEADER = sig type keywords = ((string * Position.T) * Keyword.spec) list type header = {name: string * Position.T, imports: (string * Position.T) list, keywords: keywords} val make: string * Position.T -> (string * Position.T) list -> keywords -> header val theoryN: string val bootstrap_keywords: Keyword.keywords val add_keywords: keywords -> theory -> theory val get_keywords: theory -> Keyword.keywords val get_keywords': Proof.context -> Keyword.keywords val ml_bootstrapN: string val ml_roots: string list val bootstrap_thys: string list val is_base_name: string -> bool val import_name: string -> string val args: header parser val read_tokens: Position.T -> Token.T list -> header val read: Position.T -> string -> header end; structure Thy_Header: THY_HEADER = struct (** keyword declarations **) (* header *) type keywords = ((string * Position.T) * Keyword.spec) list; type header = {name: string * Position.T, imports: (string * Position.T) list, keywords: keywords}; fun make name imports keywords : header = {name = name, imports = imports, keywords = keywords}; (* bootstrap keywords *) val chapterN = "chapter"; val sectionN = "section"; val subsectionN = "subsection"; val subsubsectionN = "subsubsection"; val paragraphN = "paragraph"; val subparagraphN = "subparagraph"; val textN = "text"; val txtN = "txt"; val text_rawN = "text_raw"; val theoryN = "theory"; val importsN = "imports"; val keywordsN = "keywords"; val abbrevsN = "abbrevs"; val beginN = "begin"; val bootstrap_keywords = Keyword.empty_keywords |> Keyword.add_keywords [(("%", \<^here>), Keyword.no_spec), (("(", \<^here>), Keyword.no_spec), ((")", \<^here>), Keyword.no_spec), ((",", \<^here>), Keyword.no_spec), (("::", \<^here>), Keyword.no_spec), (("=", \<^here>), Keyword.no_spec), (("and", \<^here>), Keyword.no_spec), ((beginN, \<^here>), Keyword.quasi_command_spec), ((importsN, \<^here>), Keyword.quasi_command_spec), ((keywordsN, \<^here>), Keyword.quasi_command_spec), ((abbrevsN, \<^here>), Keyword.quasi_command_spec), ((chapterN, \<^here>), Keyword.document_heading_spec), ((sectionN, \<^here>), Keyword.document_heading_spec), ((subsectionN, \<^here>), Keyword.document_heading_spec), ((subsubsectionN, \<^here>), Keyword.document_heading_spec), ((paragraphN, \<^here>), Keyword.document_heading_spec), ((subparagraphN, \<^here>), Keyword.document_heading_spec), ((textN, \<^here>), Keyword.document_body_spec), ((txtN, \<^here>), Keyword.document_body_spec), ((text_rawN, \<^here>), ((Keyword.document_raw, []), ["document"])), ((theoryN, \<^here>), ((Keyword.thy_begin, []), ["theory"])), (("ML", \<^here>), ((Keyword.thy_decl, []), ["ML"]))]; (* theory data *) structure Data = Theory_Data ( type T = Keyword.keywords; val empty = bootstrap_keywords; val extend = I; val merge = Keyword.merge_keywords; ); val add_keywords = Data.map o Keyword.add_keywords; val get_keywords = Data.get; val get_keywords' = get_keywords o Proof_Context.theory_of; (** concrete syntax **) (* names *) val ml_bootstrapN = "ML_Bootstrap"; val ml_roots = ["ML_Root0", "ML_Root"]; val bootstrap_thys = ["Bootstrap_Pure", "Bootstrap_ML_Bootstrap"]; fun is_base_name s = s <> "" andalso not (exists_string (member (op =) ["/", "\\", ":"]) s) fun import_name s = if String.isSuffix ".thy" s then error ("Malformed theory import: " ^ quote s) else Path.file_name (Path.explode s); (* header args *) local fun imports name = if name = Context.PureN then Scan.succeed [] else Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 Parse.theory_name); val opt_files = Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") []; val keyword_spec = Parse.group (fn () => "outer syntax keyword specification") (Parse.name -- opt_files -- Document_Source.tags); val keyword_decl = Scan.repeat1 Parse.string_position -- Scan.optional (Parse.$$$ "::" |-- Parse.!!! keyword_spec) Keyword.no_spec >> (fn (names, spec) => map (rpair spec) names); val abbrevs = Parse.and_list1 (Scan.repeat1 Parse.text -- (Parse.$$$ "=" |-- Parse.!!! (Scan.repeat1 Parse.text)) >> uncurry (map_product pair)) >> flat; val keyword_decls = Parse.and_list1 keyword_decl >> flat; in val args = Parse.theory_name :|-- (fn (name, pos) => imports name -- Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --| (Scan.optional (Parse.$$$ abbrevsN |-- Parse.!!! abbrevs) [] -- Parse.$$$ beginN) >> (fn (imports, keywords) => make (name, pos) imports keywords)); end; (* read header *) val heading = (Parse.command_name chapterN || Parse.command_name sectionN || Parse.command_name subsectionN || Parse.command_name subsubsectionN || Parse.command_name paragraphN || Parse.command_name subparagraphN || Parse.command_name textN || Parse.command_name txtN || Parse.command_name text_rawN) -- - Document_Source.annotation -- Parse.!!! Parse.document_source; + (Document_Source.annotation |-- Parse.!!! Parse.document_source); val parse_header = - (Scan.repeat heading -- Parse.command_name theoryN -- Document_Source.annotation) + (Scan.repeat heading -- Parse.command_name theoryN --| Document_Source.annotation) |-- Parse.!!! args; fun read_tokens pos toks = filter Token.is_proper toks |> Source.of_list |> Source.source Token.stopper (Scan.single (Scan.error (Parse.!!! parse_header))) |> Source.get_single |> (fn SOME (header, _) => header | NONE => error ("Unexpected end of input" ^ Position.here pos)); local fun read_header pos text = Symbol_Pos.explode (text, pos) |> Token.tokenize bootstrap_keywords {strict = false} |> read_tokens pos; val approx_length = 1024; in fun read pos text = if size text <= approx_length then read_header pos text else let val approx_text = String.substring (text, 0, approx_length) in if String.isSuffix "begin" approx_text then read_header pos text else (read_header pos approx_text handle ERROR _ => read_header pos text) end; end; end; diff --git a/src/Pure/Thy/thy_info.ML b/src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML +++ b/src/Pure/Thy/thy_info.ML @@ -1,484 +1,482 @@ (* Title: Pure/Thy/thy_info.ML Author: Markus Wenzel, TU Muenchen Global theory info database, with auto-loading according to theory and file dependencies. *) signature THY_INFO = sig type presentation_context = {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T, segments: Thy_Output.segment list} val apply_presentation: presentation_context -> theory -> unit val add_presentation: (presentation_context -> theory -> unit) -> theory -> theory val get_names: unit -> string list val lookup_theory: string -> theory option val get_theory: string -> theory val master_directory: string -> Path.T val remove_thy: string -> unit type context = {options: Options.T, symbols: HTML.symbols, bibtex_entries: string list, last_timing: Toplevel.transition -> Time.time} val use_theories: context -> string -> Path.T -> (string * Position.T) list -> unit val use_thy: string -> unit val script_thy: Position.T -> string -> theory -> theory val register_thy: theory -> unit val finish: unit -> unit end; structure Thy_Info: THY_INFO = struct (** presentation of consolidated theory **) type presentation_context = {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T, segments: Thy_Output.segment list}; structure Presentation = Theory_Data ( type T = ((presentation_context -> theory -> unit) * stamp) list; val empty = []; val extend = I; fun merge data : T = Library.merge (eq_snd op =) data; ); fun apply_presentation (context: presentation_context) thy = ignore (Presentation.get thy |> Par_List.map (fn (f, _) => f context thy)); fun add_presentation f = Presentation.map (cons (f, stamp ())); val _ = Theory.setup (add_presentation (fn {options, file_pos, segments, ...} => fn thy => if exists (Toplevel.is_skipped_proof o #state) segments then () else let val body = Thy_Output.present_thy options thy segments; val option = Present.document_option options; in if #disabled option then () else let val latex = Latex.isabelle_body (Context.theory_name thy) body; val output = [Latex.output_text latex, Latex.output_positions file_pos latex]; val _ = if Options.bool options "export_document" then Export.export thy (Path.explode "document.tex") output else (); val _ = if #enabled option then Present.theory_output thy output else (); in () end end)); (** thy database **) (* messages *) val show_path = space_implode " via " o map quote; fun cycle_msg names = "Cyclic dependency of " ^ show_path names; (* derived graph operations *) fun add_deps name parents G = String_Graph.add_deps_acyclic (name, parents) G handle String_Graph.CYCLES namess => error (cat_lines (map cycle_msg namess)); fun new_entry name parents entry = String_Graph.new_node (name, entry) #> add_deps name parents; (* global thys *) type deps = {master: (Path.T * SHA1.digest), (*master dependencies for thy file*) imports: (string * Position.T) list}; (*source specification of imports (partially qualified)*) fun make_deps master imports : deps = {master = master, imports = imports}; fun master_dir_deps (d: deps option) = the_default Path.current (Option.map (Path.dir o #1 o #master) d); local val global_thys = Synchronized.var "Thy_Info.thys" (String_Graph.empty: (deps option * theory option) String_Graph.T); in fun get_thys () = Synchronized.value global_thys; fun change_thys f = Synchronized.change global_thys f; end; fun get_names () = String_Graph.topological_order (get_thys ()); (* access thy *) fun lookup thys name = try (String_Graph.get_node thys) name; fun lookup_thy name = lookup (get_thys ()) name; fun get thys name = (case lookup thys name of SOME thy => thy | NONE => error ("Theory loader: nothing known about theory " ^ quote name)); fun get_thy name = get (get_thys ()) name; (* access deps *) val lookup_deps = Option.map #1 o lookup_thy; val master_directory = master_dir_deps o #1 o get_thy; (* access theory *) fun lookup_theory name = (case lookup_thy name of SOME (_, SOME theory) => SOME theory | _ => NONE); fun get_theory name = (case lookup_theory name of SOME theory => theory | _ => error ("Theory loader: undefined entry for theory " ^ quote name)); val get_imports = Resources.imports_of o get_theory; (** thy operations **) (* remove *) fun remove name thys = (case lookup thys name of NONE => thys | SOME (NONE, _) => error ("Cannot update finished theory " ^ quote name) | SOME _ => let val succs = String_Graph.all_succs thys [name]; val _ = writeln ("Theory loader: removing " ^ commas_quote succs); in fold String_Graph.del_node succs thys end); val remove_thy = change_thys o remove; (* update *) fun update deps theory thys = let val name = Context.theory_long_name theory; val parents = map Context.theory_long_name (Theory.parents_of theory); val thys' = remove name thys; val _ = map (get thys') parents; in new_entry name parents (SOME deps, SOME theory) thys' end; fun update_thy deps theory = change_thys (update deps theory); (* context *) type context = {options: Options.T, symbols: HTML.symbols, bibtex_entries: string list, last_timing: Toplevel.transition -> Time.time}; fun default_context (): context = {options = Options.default (), symbols = HTML.no_symbols, bibtex_entries = [], last_timing = K Time.zeroTime}; (* scheduling loader tasks *) datatype result = Result of {theory: theory, exec_id: Document_ID.exec, present: unit -> unit, commit: unit -> unit, weight: int}; fun theory_result theory = Result {theory = theory, exec_id = Document_ID.none, present = I, commit = I, weight = 0}; fun result_theory (Result {theory, ...}) = theory; fun result_present (Result {present, ...}) = present; fun result_commit (Result {commit, ...}) = commit; fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i); fun join_theory (Result {theory, exec_id, ...}) = let val _ = Execution.join [exec_id]; val res = Exn.capture Thm.consolidate_theory theory; val exns = maps Task_Queue.group_status (Execution.peek exec_id); in res :: map Exn.Exn exns end; datatype task = Task of string list * (theory list -> result) | Finished of theory; fun task_finished (Task _) = false | task_finished (Finished _) = true; fun task_parents deps (parents: string list) = map (the o AList.lookup (op =) deps) parents; val schedule_seq = String_Graph.schedule (fn deps => fn (_, task) => (case task of Task (parents, body) => let val result = body (task_parents deps parents); val _ = Par_Exn.release_all (join_theory result); val _ = result_present result (); val _ = result_commit result (); in result_theory result end | Finished thy => thy)) #> ignore; val schedule_futures = Thread_Attributes.uninterruptible (fn _ => fn tasks => let val futures = tasks |> String_Graph.schedule (fn deps => fn (name, task) => (case task of Task (parents, body) => (singleton o Future.forks) {name = "theory:" ^ name, group = NONE, deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true} (fn () => (case filter (not o can Future.join o #2) deps of [] => body (map (result_theory o Future.join) (task_parents deps parents)) | bad => error ("Failed to load theory " ^ quote name ^ " (unresolved " ^ commas_quote (map #1 bad) ^ ")"))) | Finished theory => Future.value (theory_result theory))); val results1 = futures |> maps (fn future => (case Future.join_result future of Exn.Res result => join_theory result | Exn.Exn exn => [Exn.Exn exn])); val results2 = futures |> map_filter (Exn.get_res o Future.join_result) |> sort result_ord |> Par_List.map (fn result => Exn.capture (result_present result) ()); (* FIXME more precise commit order (!?) *) val results3 = futures |> map (fn future => Exn.capture (fn () => result_commit (Future.join future) ()) ()); (* FIXME avoid global Execution.reset (!??) *) val results4 = map Exn.Exn (maps Task_Queue.group_status (Execution.reset ())); val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4); in () end); (* eval theory *) fun excursion keywords master_dir last_timing init elements = let fun prepare_span st span = Command_Span.content span |> Command.read keywords (Command.read_thy st) master_dir init ([], ~1) |> (fn tr => Toplevel.timing (last_timing tr) tr); fun element_result span_elem (st, _) = let val elem = Thy_Element.map_element (prepare_span st) span_elem; val (results, st') = Toplevel.element_result keywords elem st; val pos' = Toplevel.pos_of (Thy_Element.last_element elem); in (results, (st', pos')) end; val (results, (end_state, end_pos)) = fold_map element_result elements (Toplevel.init_toplevel (), Position.none); val thy = Toplevel.end_theory end_pos end_state; in (results, thy) end; fun eval_thy (context: context) update_time master_dir header text_pos text parents = let val {options, symbols, bibtex_entries, last_timing} = context; val (name, _) = #name header; val keywords = fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents (Keyword.add_keywords (#keywords header) Keyword.empty_keywords); val spans = Outer_Syntax.parse_spans (Token.explode keywords text_pos text); val elements = Thy_Element.parse_elements keywords spans; fun init () = Resources.begin_theory master_dir header parents |> Present.begin_theory bibtex_entries update_time (fn () => implode (map (HTML.present_span symbols keywords) spans)); val (results, thy) = cond_timeit true ("theory " ^ quote name) (fn () => excursion keywords master_dir last_timing init elements); fun present () = let val segments = (spans ~~ maps Toplevel.join_results results) |> map (fn (span, (tr, st')) => {span = span, command = tr, state = st'}); val context: presentation_context = {options = options, file_pos = text_pos, adjust_pos = I, segments = segments}; in apply_presentation context thy end; in (thy, present, size text) end; (* require_thy -- checking database entries wrt. the file-system *) local fun required_by _ [] = "" | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")"; fun load_thy context initiators update_time deps text (name, pos) keywords parents = let val _ = remove_thy name; val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators); val _ = Output.try_protocol_message (Markup.loading_theory name) []; val {master = (thy_path, _), imports} = deps; val dir = Path.dir thy_path; val header = Thy_Header.make (name, pos) imports keywords; val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents); val exec_id = Document_ID.make (); val _ = Execution.running Document_ID.none exec_id [] orelse raise Fail ("Failed to register execution: " ^ Document_ID.print exec_id); val timing_start = Timing.start (); val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path); val (theory, present, weight) = eval_thy context update_time dir header text_pos text (if name = Context.PureN then [Context.the_global_context ()] else parents); val timing_result = Timing.result timing_start; val timing_props = [Markup.theory_timing, (Markup.nameN, name)]; val _ = Output.try_protocol_message (timing_props @ Markup.timing_properties timing_result) [] fun commit () = update_thy deps theory; in Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight} end; fun check_deps dir name = (case lookup_deps name of SOME NONE => (true, NONE, Position.none, get_imports name, []) | NONE => let val {master, text, theory_pos, imports, keywords} = Resources.check_thy dir name in (false, SOME (make_deps master imports, text), theory_pos, imports, keywords) end | SOME (SOME {master, ...}) => let val {master = master', text = text', theory_pos = theory_pos', imports = imports', keywords = keywords'} = Resources.check_thy dir name; val deps' = SOME (make_deps master' imports', text'); val current = #2 master = #2 master' andalso (case lookup_theory name of NONE => false | SOME theory => Resources.loaded_files_current theory); in (current, deps', theory_pos', imports', keywords') end); in fun require_thys context initiators qualifier dir strs tasks = fold_map (require_thy context initiators qualifier dir) strs tasks |>> forall I and require_thy context initiators qualifier dir (s, require_pos) tasks = let val {master_dir, theory_name, ...} = Resources.import_name qualifier dir s; in (case try (String_Graph.get_node tasks) theory_name of SOME task => (task_finished task, tasks) | NONE => let val _ = member (op =) initiators theory_name andalso error (cycle_msg initiators); val (current, deps, theory_pos, imports, keywords) = check_deps master_dir theory_name handle ERROR msg => cat_error msg ("The error(s) above occurred for theory " ^ quote theory_name ^ Position.here require_pos ^ required_by "\n" initiators); val qualifier' = Resources.theory_qualifier theory_name; val dir' = Path.append dir (master_dir_deps (Option.map #1 deps)); val parents = map (#theory_name o Resources.import_name qualifier' dir' o #1) imports; val (parents_current, tasks') = require_thys context (theory_name :: initiators) qualifier' dir' imports tasks; val all_current = current andalso parents_current; val task = if all_current then Finished (get_theory theory_name) else (case deps of NONE => raise Fail "Malformed deps" | SOME (dep, text) => let val update_time = serial (); val load = load_thy context initiators update_time dep text (theory_name, theory_pos) keywords; in Task (parents, load) end); val tasks'' = new_entry theory_name parents task tasks'; in (all_current, tasks'') end) end; end; (* use theories *) fun use_theories context qualifier master_dir imports = let val (_, tasks) = require_thys context [] qualifier master_dir imports String_Graph.empty in if Multithreading.max_threads () > 1 then schedule_futures tasks else schedule_seq tasks end; fun use_thy name = use_theories (default_context ()) Resources.default_qualifier Path.current [(name, Position.none)]; (* toplevel scripting -- without maintaining database *) fun script_thy pos txt thy = let - val trs = - Outer_Syntax.parse thy pos txt - |> map (Toplevel.modify_init (K thy)); + val trs = Outer_Syntax.parse_text thy (K thy) pos txt; val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs); val end_state = fold (Toplevel.command_exception true) trs (Toplevel.init_toplevel ()); in Toplevel.end_theory end_pos end_state end; (* register theory *) fun register_thy theory = let val name = Context.theory_long_name theory; val {master, ...} = Resources.check_thy (Resources.master_directory theory) name; val imports = Resources.imports_of theory; in change_thys (fn thys => let val thys' = remove name thys; val _ = writeln ("Registering theory " ^ quote name); in update (make_deps master imports) theory thys' end) end; (* finish all theories *) fun finish () = change_thys (String_Graph.map (fn _ => fn (_, entry) => (NONE, entry))); end; fun use_thy name = Runtime.toplevel_program (fn () => Thy_Info.use_thy name); diff --git a/src/Pure/Thy/thy_output.ML b/src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML +++ b/src/Pure/Thy/thy_output.ML @@ -1,556 +1,557 @@ (* Title: Pure/Thy/thy_output.ML Author: Makarius Theory document output. *) signature THY_OUTPUT = sig val output_document: Proof.context -> {markdown: bool} -> Input.source -> Latex.text list val check_comments: Proof.context -> Symbol_Pos.T list -> unit val output_token: Proof.context -> Token.T -> Latex.text list val output_source: Proof.context -> string -> Latex.text list type segment = {span: Command_Span.span, command: Toplevel.transition, state: Toplevel.state} val present_thy: Options.T -> theory -> segment list -> Latex.text list val pretty_term: Proof.context -> term -> Pretty.T val pretty_thm: Proof.context -> thm -> Pretty.T val lines: Latex.text list -> Latex.text list val items: Latex.text list -> Latex.text list val isabelle: Proof.context -> Latex.text list -> Latex.text val isabelle_typewriter: Proof.context -> Latex.text list -> Latex.text val typewriter: Proof.context -> string -> Latex.text val verbatim: Proof.context -> string -> Latex.text val source: Proof.context -> Token.src -> Latex.text val pretty: Proof.context -> Pretty.T -> Latex.text val pretty_source: Proof.context -> Token.src -> Pretty.T -> Latex.text val pretty_items: Proof.context -> Pretty.T list -> Latex.text val pretty_items_source: Proof.context -> Token.src -> Pretty.T list -> Latex.text val antiquotation_pretty: binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory val antiquotation_pretty_embedded: binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory val antiquotation_pretty_source: binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory val antiquotation_pretty_source_embedded: binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory val antiquotation_raw: binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory val antiquotation_raw_embedded: binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory val antiquotation_verbatim: binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory val antiquotation_verbatim_embedded: binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory end; structure Thy_Output: THY_OUTPUT = struct (* output document source *) val output_symbols = single o Latex.symbols_output; fun output_comment ctxt (kind, syms) = (case kind of Comment.Comment => Input.cartouche_content syms |> output_document (ctxt |> Config.put Document_Antiquotation.thy_output_display false) {markdown = false} |> Latex.enclose_body "%\n\\isamarkupcmt{" "%\n}" | Comment.Cancel => Symbol_Pos.cartouche_content syms |> output_symbols |> Latex.enclose_body "%\n\\isamarkupcancel{" "}" - | Comment.Latex => - [Latex.symbols (Symbol_Pos.cartouche_content syms)]) + | Comment.Latex => [Latex.symbols (Symbol_Pos.cartouche_content syms)] + | Comment.Marker => []) and output_comment_document ctxt (comment, syms) = (case comment of SOME kind => output_comment ctxt (kind, syms) | NONE => [Latex.symbols syms]) and output_document_text ctxt syms = Comment.read_body syms |> maps (output_comment_document ctxt) and output_document ctxt {markdown} source = let val pos = Input.pos_of source; val syms = Input.source_explode source; val output_antiquotes = maps (Document_Antiquotation.evaluate (output_document_text ctxt) ctxt); fun output_line line = (if Markdown.line_is_item line then [Latex.string "\\item "] else []) @ output_antiquotes (Markdown.line_content line); fun output_block (Markdown.Par lines) = Latex.block (separate (Latex.string "\n") (map (Latex.block o output_line) lines)) | output_block (Markdown.List {kind, body, ...}) = Latex.environment_block (Markdown.print_kind kind) (output_blocks body) and output_blocks blocks = separate (Latex.string "\n\n") (map output_block blocks); in if Toplevel.is_skipped_proof (Toplevel.presentation_state ctxt) then [] else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms then let val ants = Antiquote.parse_comments pos syms; val reports = Antiquote.antiq_reports ants; val blocks = Markdown.read_antiquotes ants; val _ = Context_Position.reports ctxt (reports @ Markdown.reports blocks); in output_blocks blocks end else let val ants = Antiquote.parse_comments pos (trim (Symbol.is_blank o Symbol_Pos.symbol) syms); val reports = Antiquote.antiq_reports ants; val _ = Context_Position.reports ctxt (reports @ Markdown.text_reports ants); in output_antiquotes ants end end; (* output tokens with formal comments *) local val output_symbols_antiq = (fn Antiquote.Text syms => output_symbols syms | Antiquote.Control {name = (name, _), body, ...} => Latex.string (Latex.output_symbols [Symbol.encode (Symbol.Control name)]) :: output_symbols body | Antiquote.Antiq {body, ...} => Latex.enclose_body "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n" (output_symbols body)); fun output_comment_symbols ctxt {antiq} (comment, syms) = (case (comment, antiq) of (NONE, false) => output_symbols syms | (NONE, true) => Antiquote.parse_comments (#1 (Symbol_Pos.range syms)) syms |> maps output_symbols_antiq | (SOME comment, _) => output_comment ctxt (comment, syms)); fun output_body ctxt antiq bg en syms = Comment.read_body syms |> maps (output_comment_symbols ctxt {antiq = antiq}) |> Latex.enclose_body bg en; in fun output_token ctxt tok = let fun output antiq bg en = output_body ctxt antiq bg en (Input.source_explode (Token.input_of tok)); in (case Token.kind_of tok of Token.Comment NONE => [] + | Token.Comment (SOME Comment.Marker) => [] | Token.Command => output false "\\isacommand{" "}" | Token.Keyword => if Symbol.is_ascii_identifier (Token.content_of tok) then output false "\\isakeyword{" "}" else output false "" "" | Token.String => output false "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" | Token.Alt_String => output false "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" | Token.Verbatim => output true "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" | Token.Cartouche => output false "{\\isacartoucheopen}" "{\\isacartoucheclose}" | _ => output false "" "") end handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok)); fun output_source ctxt s = output_body ctxt false "" "" (Symbol_Pos.explode (s, Position.none)); fun check_comments ctxt = Comment.read_body #> List.app (fn (comment, syms) => let val pos = #1 (Symbol_Pos.range syms); val _ = comment |> Option.app (fn kind => Context_Position.reports ctxt (map (pair pos) (Markup.cartouche :: Comment.markups kind))); val _ = output_comment_symbols ctxt {antiq = false} (comment, syms); in if comment = SOME Comment.Comment then check_comments ctxt syms else () end); end; (** present theory source **) (* presentation tokens *) datatype token = Ignore_Token | Basic_Token of Token.T | Markup_Token of string * Input.source | Markup_Env_Token of string * Input.source | Raw_Token of Input.source; fun basic_token pred (Basic_Token tok) = pred tok | basic_token _ _ = false; val white_token = basic_token Document_Source.is_white; val white_comment_token = basic_token Document_Source.is_white_comment; val blank_token = basic_token Token.is_blank; val newline_token = basic_token Token.is_newline; fun present_token ctxt tok = (case tok of Ignore_Token => [] | Basic_Token tok => output_token ctxt tok | Markup_Token (cmd, source) => Latex.enclose_body ("%\n\\isamarkup" ^ cmd ^ "{") "%\n}\n" (output_document ctxt {markdown = false} source) | Markup_Env_Token (cmd, source) => [Latex.environment_block ("isamarkup" ^ cmd) (output_document ctxt {markdown = true} source)] | Raw_Token source => Latex.string "%\n" :: output_document ctxt {markdown = true} source @ [Latex.string "\n"]); (* command spans *) type command = string * Position.T; (*name, position*) type source = (token * (string * int)) list; (*token, markup flag, meta-comment depth*) datatype span = Span of command * (source * source * source * source) * bool; fun make_span cmd src = let fun chop_newline (tok :: toks) = if newline_token (fst tok) then ([tok], toks, true) else ([], tok :: toks, false) | chop_newline [] = ([], [], false); val (((src_prefix, src_main), src_suffix1), (src_suffix2, src_appendix, newline)) = src |> chop_prefix (white_token o fst) ||>> chop_suffix (white_token o fst) ||>> chop_prefix (white_comment_token o fst) ||> chop_newline; in Span (cmd, (src_prefix, src_main, src_suffix1 @ src_suffix2, src_appendix), newline) end; (* present spans *) local fun err_bad_nesting pos = error ("Bad nesting of commands in presentation" ^ pos); fun edge which f (x: string option, y) = if x = y then I else (case which (x, y) of NONE => I | SOME txt => cons (Latex.string (f txt))); val begin_tag = edge #2 Latex.begin_tag; val end_tag = edge #1 Latex.end_tag; fun open_delim delim e = edge #2 Latex.begin_delim e #> delim #> edge #2 Latex.end_delim e; fun close_delim delim e = edge #1 Latex.begin_delim e #> delim #> edge #1 Latex.end_delim e; fun read_tag s = (case space_explode "%" s of ["", b] => (SOME b, NONE) | [a, b] => (NONE, SOME (a, b)) | _ => error ("Bad document_tags specification: " ^ quote s)); in fun make_command_tag options keywords = let val document_tags = map read_tag (space_explode "," (Options.string options \<^system_option>\document_tags\)); val document_tags_default = map_filter #1 document_tags; val document_tags_command = map_filter #2 document_tags; in fn {cmd_name, cmd_tags, tag, active_tag} => fn state => fn state' => let val tag' = try hd (fold (update (op =)) cmd_tags (the_list tag)); val keyword_tags = if cmd_name = "end" andalso Toplevel.is_end_theory state' then ["theory"] else Keyword.command_tags keywords cmd_name; val command_tags = the_list (AList.lookup (op =) document_tags_command cmd_name) @ keyword_tags @ document_tags_default; val active_tag' = if is_some tag' then tag' else (case command_tags of default_tag :: _ => SOME default_tag | [] => if Keyword.is_vacuous keywords cmd_name andalso Toplevel.is_proof state then active_tag else NONE); in {tag' = tag', active_tag' = active_tag'} end end; fun present_span thy command_tag span state state' (tag_stack, active_tag, newline, latex, present_cont) = let val ctxt' = Toplevel.presentation_context state' handle Toplevel.UNDEF => Proof_Context.get_global thy Context.PureN; val present = fold (fn (tok, (flag, 0)) => fold cons (present_token ctxt' tok) #> cons (Latex.string flag) | _ => I); val Span ((cmd_name, cmd_pos), srcs, span_newline) = span; val cmd_tags = Document_Source.get_tags (Toplevel.presentation_context state'); val (tag, tags) = tag_stack; val {tag', active_tag'} = command_tag {cmd_name = cmd_name, cmd_tags = cmd_tags, tag = tag, active_tag = active_tag} state state'; val edge = (active_tag, active_tag'); val nesting = Toplevel.level state' - Toplevel.level state; val newline' = if is_none active_tag' then span_newline else newline; val tag_stack' = if nesting = 0 andalso not (Toplevel.is_proof state) then tag_stack else if nesting >= 0 then (tag', replicate nesting tag @ tags) else (case drop (~ nesting - 1) tags of tg :: tgs => (tg, tgs) | [] => err_bad_nesting (Position.here cmd_pos)); val latex' = latex |> end_tag edge |> close_delim (fst present_cont) edge |> snd present_cont |> open_delim (present (#1 srcs)) edge |> begin_tag edge |> present (#2 srcs); val present_cont' = if newline then (present (#3 srcs), present (#4 srcs)) else (I, present (#3 srcs) #> present (#4 srcs)); in (tag_stack', active_tag', newline', latex', present_cont') end; fun present_trailer ((_, tags), active_tag, _, latex, present_cont) = if not (null tags) then err_bad_nesting " at end of theory" else latex |> end_tag (active_tag, NONE) |> close_delim (fst present_cont) (active_tag, NONE) |> snd present_cont; end; (* present_thy *) local val markup_true = "\\isamarkuptrue%\n"; val markup_false = "\\isamarkupfalse%\n"; val opt_newline = Scan.option (Scan.one Token.is_newline); val ignore = Scan.depend (fn d => opt_newline |-- Scan.one Token.is_begin_ignore >> pair (d + 1)) || Scan.depend (fn d => Scan.one Token.is_end_ignore --| (if d = 0 then Scan.fail_with (K (fn () => "Bad nesting of meta-comments")) else opt_newline) >> pair (d - 1)); val locale = Scan.option ((Parse.$$$ "(" -- Document_Source.improper -- Parse.$$$ "in") |-- Parse.!!! (Document_Source.improper |-- Parse.name --| (Document_Source.improper -- Parse.$$$ ")"))); in type segment = {span: Command_Span.span, command: Toplevel.transition, state: Toplevel.state}; fun present_thy options thy (segments: segment list) = let val keywords = Thy_Header.get_keywords thy; (* tokens *) val ignored = Scan.state --| ignore >> (fn d => (NONE, (Ignore_Token, ("", d)))); fun markup pred mk flag = Scan.peek (fn d => Document_Source.improper |-- Parse.position (Scan.one (fn tok => Token.is_command tok andalso pred keywords (Token.content_of tok))) -- (Document_Source.annotation |-- Parse.!!!! ((Document_Source.improper -- locale -- Document_Source.improper) |-- Parse.document_source --| Document_Source.improper_end)) >> (fn ((tok, pos'), source) => let val name = Token.content_of tok in (SOME (name, pos'), (mk (name, source), (flag, d))) end)); val command = Scan.peek (fn d => Scan.optional (Scan.one Token.is_command_modifier ::: Document_Source.improper) [] -- Scan.one Token.is_command --| Document_Source.annotation >> (fn (cmd_mod, cmd) => map (fn tok => (NONE, (Basic_Token tok, ("", d)))) cmd_mod @ [(SOME (Token.content_of cmd, Token.pos_of cmd), (Basic_Token cmd, (markup_false, d)))])); val cmt = Scan.peek (fn d => Scan.one Document_Source.is_black_comment >> (fn tok => (NONE, (Basic_Token tok, ("", d))))); val other = Scan.peek (fn d => Parse.not_eof >> (fn tok => (NONE, (Basic_Token tok, ("", d))))); val tokens = (ignored || markup Keyword.is_document_heading Markup_Token markup_true || markup Keyword.is_document_body Markup_Env_Token markup_true || markup Keyword.is_document_raw (Raw_Token o #2) "") >> single || command || (cmt || other) >> single; (* spans *) val is_eof = fn (_, (Basic_Token x, _)) => Token.is_eof x | _ => false; val stopper = Scan.stopper (K (NONE, (Basic_Token Token.eof, ("", 0)))) is_eof; val cmd = Scan.one (is_some o fst); val non_cmd = Scan.one (is_none o fst andf not o is_eof) >> #2; val white_comments = Scan.many (white_comment_token o fst o snd); val blank = Scan.one (blank_token o fst o snd); val newline = Scan.one (newline_token o fst o snd); val before_cmd = Scan.option (newline -- white_comments) -- Scan.option (newline -- white_comments) -- Scan.option (blank -- white_comments) -- cmd; val span = Scan.repeat non_cmd -- cmd -- Scan.repeat (Scan.unless before_cmd non_cmd) -- Scan.option (newline >> (single o snd)) >> (fn (((toks1, (cmd, tok2)), toks3), tok4) => make_span (the cmd) (toks1 @ (tok2 :: (toks3 @ the_default [] tok4)))); val spans = segments |> maps (Command_Span.content o #span) |> drop_suffix Token.is_space |> Source.of_list |> Source.source' 0 Token.stopper (Scan.error (Scan.bulk tokens >> flat)) |> Source.source stopper (Scan.error (Scan.bulk span)) |> Source.exhaust; val command_results = segments |> map_filter (fn {command, state, ...} => if Toplevel.is_ignored command then NONE else SOME (command, state)); (* present commands *) val command_tag = make_command_tag options keywords; fun present_command tr span st st' = Toplevel.setmp_thread_position tr (present_span thy command_tag span st st'); fun present _ [] = I | present st ((span, (tr, st')) :: rest) = present_command tr span st st' #> present st' rest; in if length command_results = length spans then ((NONE, []), NONE, true, [], (I, I)) |> present (Toplevel.init_toplevel ()) (spans ~~ command_results) |> present_trailer |> rev else error "Messed-up outer syntax for presentation" end; end; (** standard output operations **) (* pretty printing *) fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t; fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of; (* default output *) val lines = separate (Latex.string "\\isanewline%\n"); val items = separate (Latex.string "\\isasep\\isanewline%\n"); fun isabelle ctxt body = if Config.get ctxt Document_Antiquotation.thy_output_display then Latex.environment_block "isabelle" body else Latex.block (Latex.enclose_body "\\isa{" "}" body); fun isabelle_typewriter ctxt body = if Config.get ctxt Document_Antiquotation.thy_output_display then Latex.environment_block "isabellett" body else Latex.block (Latex.enclose_body "\\isatt{" "}" body); fun typewriter ctxt s = isabelle_typewriter ctxt [Latex.string (Latex.output_ascii s)]; fun verbatim ctxt = if Config.get ctxt Document_Antiquotation.thy_output_display then Document_Antiquotation.indent_lines ctxt #> typewriter ctxt else split_lines #> map (typewriter ctxt) #> lines #> Latex.block; fun source ctxt = Token.args_of_src #> map (Token.unparse #> Document_Antiquotation.prepare_lines ctxt) #> space_implode " " #> output_source ctxt #> isabelle ctxt; fun pretty ctxt = Document_Antiquotation.output ctxt #> Latex.string #> single #> isabelle ctxt; fun pretty_source ctxt src prt = if Config.get ctxt Document_Antiquotation.thy_output_source then source ctxt src else pretty ctxt prt; fun pretty_items ctxt = map (Document_Antiquotation.output ctxt #> Latex.string) #> items #> isabelle ctxt; fun pretty_items_source ctxt src prts = if Config.get ctxt Document_Antiquotation.thy_output_source then source ctxt src else pretty_items ctxt prts; (* antiquotation variants *) local fun gen_setup name embedded = if embedded then Document_Antiquotation.setup_embedded name else Document_Antiquotation.setup name; fun gen_antiquotation_pretty name embedded scan f = gen_setup name embedded scan (fn {context = ctxt, argument = x, ...} => pretty ctxt (f ctxt x)); fun gen_antiquotation_pretty_source name embedded scan f = gen_setup name embedded scan (fn {context = ctxt, source = src, argument = x} => pretty_source ctxt src (f ctxt x)); fun gen_antiquotation_raw name embedded scan f = gen_setup name embedded scan (fn {context = ctxt, argument = x, ...} => f ctxt x); fun gen_antiquotation_verbatim name embedded scan f = gen_antiquotation_raw name embedded scan (fn ctxt => verbatim ctxt o f ctxt); in fun antiquotation_pretty name = gen_antiquotation_pretty name false; fun antiquotation_pretty_embedded name = gen_antiquotation_pretty name true; fun antiquotation_pretty_source name = gen_antiquotation_pretty_source name false; fun antiquotation_pretty_source_embedded name = gen_antiquotation_pretty_source name true; fun antiquotation_raw name = gen_antiquotation_raw name false; fun antiquotation_raw_embedded name = gen_antiquotation_raw name true; fun antiquotation_verbatim name = gen_antiquotation_verbatim name false; fun antiquotation_verbatim_embedded name = gen_antiquotation_verbatim name true; end; end; diff --git a/src/Pure/Tools/rail.ML b/src/Pure/Tools/rail.ML --- a/src/Pure/Tools/rail.ML +++ b/src/Pure/Tools/rail.ML @@ -1,392 +1,392 @@ (* Title: Pure/Tools/rail.ML Author: Michael Kerscher, TU München Author: Makarius Railroad diagrams in LaTeX. *) signature RAIL = sig datatype rails = Cat of int * rail list and rail = Bar of rails list | Plus of rails * rails | Newline of int | Nonterminal of string | Terminal of bool * string | Antiquote of bool * Antiquote.antiq val read: Proof.context -> Input.source -> (string Antiquote.antiquote * rail) list val output_rules: Proof.context -> (string Antiquote.antiquote * rail) list -> Latex.text end; structure Rail: RAIL = struct (** lexical syntax **) (* singleton keywords *) val keywords = Symtab.make [ ("|", Markup.keyword3), ("*", Markup.keyword3), ("+", Markup.keyword3), ("?", Markup.keyword3), ("(", Markup.empty), (")", Markup.empty), ("\", Markup.keyword2), (";", Markup.keyword2), (":", Markup.keyword2), ("@", Markup.keyword1)]; (* datatype token *) datatype kind = Keyword | Ident | String | Space | Comment of Comment.kind | Antiq of Antiquote.antiq | EOF; datatype token = Token of Position.range * (kind * string); fun pos_of (Token ((pos, _), _)) = pos; fun end_pos_of (Token ((_, pos), _)) = pos; fun range_of (toks as tok :: _) = let val pos' = end_pos_of (List.last toks) in Position.range (pos_of tok, pos') end | range_of [] = Position.no_range; fun kind_of (Token (_, (k, _))) = k; fun content_of (Token (_, (_, x))) = x; fun is_proper (Token (_, (Space, _))) = false | is_proper (Token (_, (Comment _, _))) = false | is_proper _ = true; (* diagnostics *) val print_kind = fn Keyword => "rail keyword" | Ident => "identifier" | String => "single-quoted string" | Space => "white space" | Comment _ => "formal comment" | Antiq _ => "antiquotation" | EOF => "end-of-input"; fun print (Token ((pos, _), (k, x))) = (if k = EOF then print_kind k else print_kind k ^ " " ^ quote x) ^ Position.here pos; fun print_keyword x = print_kind Keyword ^ " " ^ quote x; fun reports_of_token (Token ((pos, _), (Keyword, x))) = map (pair pos) (the_list (Symtab.lookup keywords x) @ Completion.suppress_abbrevs x) | reports_of_token (Token ((pos, _), (String, _))) = [(pos, Markup.inner_string)] | reports_of_token (Token (_, (Antiq antiq, _))) = Antiquote.antiq_reports [Antiquote.Antiq antiq] | reports_of_token _ = []; (* stopper *) fun mk_eof pos = Token ((pos, Position.none), (EOF, "")); val eof = mk_eof Position.none; fun is_eof (Token (_, (EOF, _))) = true | is_eof _ = false; val stopper = Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof; (* tokenize *) local fun token k ss = [Token (Symbol_Pos.range ss, (k, Symbol_Pos.content ss))]; fun antiq_token antiq = [Token (#range antiq, (Antiq antiq, Symbol_Pos.content (#body antiq)))]; val scan_space = Scan.many1 (Symbol.is_blank o Symbol_Pos.symbol); val scan_keyword = Scan.one (Symtab.defined keywords o Symbol_Pos.symbol); val err_prefix = "Rail lexical error: "; val scan_token = scan_space >> token Space || - Comment.scan >> (fn (kind, ss) => token (Comment kind) ss)|| + Comment.scan_inner >> (fn (kind, ss) => token (Comment kind) ss) || Antiquote.scan_antiq >> antiq_token || scan_keyword >> (token Keyword o single) || Lexicon.scan_id >> token Ident || Symbol_Pos.scan_string_q err_prefix >> (fn (pos1, (ss, pos2)) => [Token (Position.range (pos1, pos2), (String, Symbol_Pos.content ss))]); val scan = Scan.repeats scan_token --| Symbol_Pos.!!! (fn () => err_prefix ^ "bad input") (Scan.ahead (Scan.one Symbol_Pos.is_eof)); in val tokenize = #1 o Scan.error (Scan.finite Symbol_Pos.stopper scan); end; (** parsing **) (* parser combinators *) fun !!! scan = let val prefix = "Rail syntax error"; fun get_pos [] = " (end-of-input)" | get_pos (tok :: _) = Position.here (pos_of tok); fun err (toks, NONE) = (fn () => prefix ^ get_pos toks) | err (toks, SOME msg) = (fn () => let val s = msg () in if String.isPrefix prefix s then s else prefix ^ get_pos toks ^ ": " ^ s end); in Scan.!! err scan end; fun $$$ x = Scan.one (fn tok => kind_of tok = Keyword andalso content_of tok = x) || Scan.fail_with (fn [] => (fn () => print_keyword x ^ " expected,\nbut end-of-input was found") | tok :: _ => (fn () => print_keyword x ^ " expected,\nbut " ^ print tok ^ " was found")); fun enum1 sep scan = scan ::: Scan.repeat ($$$ sep |-- !!! scan); fun enum sep scan = enum1 sep scan || Scan.succeed []; val ident = Scan.some (fn tok => if kind_of tok = Ident then SOME (content_of tok) else NONE); val string = Scan.some (fn tok => if kind_of tok = String then SOME (content_of tok) else NONE); val antiq = Scan.some (fn tok => (case kind_of tok of Antiq a => SOME a | _ => NONE)); fun RANGE scan = Scan.trace scan >> apsnd range_of; fun RANGE_APP scan = RANGE scan >> (fn (f, r) => f r); (* parse trees *) datatype trees = CAT of tree list * Position.range and tree = BAR of trees list * Position.range | STAR of (trees * trees) * Position.range | PLUS of (trees * trees) * Position.range | MAYBE of tree * Position.range | NEWLINE of Position.range | NONTERMINAL of string * Position.range | TERMINAL of (bool * string) * Position.range | ANTIQUOTE of (bool * Antiquote.antiq) * Position.range; fun reports_of_tree ctxt = if Context_Position.is_visible ctxt then let fun reports r = if r = Position.no_range then [] else [(Position.range_position r, Markup.expression "")]; fun trees (CAT (ts, r)) = reports r @ maps tree ts and tree (BAR (Ts, r)) = reports r @ maps trees Ts | tree (STAR ((T1, T2), r)) = reports r @ trees T1 @ trees T2 | tree (PLUS ((T1, T2), r)) = reports r @ trees T1 @ trees T2 | tree (MAYBE (t, r)) = reports r @ tree t | tree (NEWLINE r) = reports r | tree (NONTERMINAL (_, r)) = reports r | tree (TERMINAL (_, r)) = reports r | tree (ANTIQUOTE (_, r)) = reports r; in distinct (op =) o tree end else K []; local val at_mode = Scan.option ($$$ "@") >> (fn NONE => false | _ => true); fun body x = (RANGE (enum1 "|" body1) >> BAR) x and body0 x = (RANGE (enum "|" body1) >> BAR) x and body1 x = (RANGE_APP (body2 :|-- (fn a => $$$ "*" |-- !!! body4e >> (fn b => fn r => CAT ([STAR ((a, b), r)], r)) || $$$ "+" |-- !!! body4e >> (fn b => fn r => CAT ([PLUS ((a, b), r)], r)) || Scan.succeed (K a)))) x and body2 x = (RANGE (Scan.repeat1 body3) >> CAT) x and body3 x = (RANGE_APP (body4 :|-- (fn a => $$$ "?" >> K (curry MAYBE a) || Scan.succeed (K a)))) x and body4 x = ($$$ "(" |-- !!! (body0 --| $$$ ")") || RANGE_APP ($$$ "\" >> K NEWLINE || ident >> curry NONTERMINAL || at_mode -- string >> curry TERMINAL || at_mode -- antiq >> curry ANTIQUOTE)) x and body4e x = (RANGE (Scan.option body4) >> (fn (a, r) => CAT (the_list a, r))) x; val rule_name = ident >> Antiquote.Text || antiq >> Antiquote.Antiq; val rule = rule_name -- ($$$ ":" |-- !!! body) || body >> pair (Antiquote.Text ""); val rules = enum1 ";" (Scan.option rule) >> map_filter I; in fun parse_rules toks = #1 (Scan.error (Scan.finite stopper (rules --| !!! (Scan.ahead (Scan.one is_eof)))) toks); end; (** rail expressions **) (* datatype *) datatype rails = Cat of int * rail list and rail = Bar of rails list | Plus of rails * rails | Newline of int | Nonterminal of string | Terminal of bool * string | Antiquote of bool * Antiquote.antiq; fun is_newline (Newline _) = true | is_newline _ = false; (* prepare *) local fun cat rails = Cat (0, rails); val empty = cat []; fun is_empty (Cat (_, [])) = true | is_empty _ = false; fun bar [Cat (_, [rail])] = rail | bar cats = Bar cats; fun reverse_cat (Cat (y, rails)) = Cat (y, rev (map reverse rails)) and reverse (Bar cats) = Bar (map reverse_cat cats) | reverse (Plus (cat1, cat2)) = Plus (reverse_cat cat1, reverse_cat cat2) | reverse x = x; fun plus (cat1, cat2) = Plus (cat1, reverse_cat cat2); in fun prepare_trees (CAT (ts, _)) = Cat (0, map prepare_tree ts) and prepare_tree (BAR (Ts, _)) = bar (map prepare_trees Ts) | prepare_tree (STAR (Ts, _)) = let val (cat1, cat2) = apply2 prepare_trees Ts in if is_empty cat2 then plus (empty, cat1) else bar [empty, cat [plus (cat1, cat2)]] end | prepare_tree (PLUS (Ts, _)) = plus (apply2 prepare_trees Ts) | prepare_tree (MAYBE (t, _)) = bar [empty, cat [prepare_tree t]] | prepare_tree (NEWLINE _) = Newline 0 | prepare_tree (NONTERMINAL (a, _)) = Nonterminal a | prepare_tree (TERMINAL (a, _)) = Terminal a | prepare_tree (ANTIQUOTE (a, _)) = Antiquote a; end; (* read *) fun read ctxt source = let val _ = Context_Position.report ctxt (Input.pos_of source) Markup.language_rail; val toks = tokenize (Input.source_explode source); val _ = Context_Position.reports ctxt (maps reports_of_token toks); val rules = parse_rules (filter is_proper toks); val _ = Position.reports (maps (reports_of_tree ctxt o #2) rules); in map (apsnd prepare_tree) rules end; (* latex output *) local fun vertical_range_cat (Cat (_, rails)) y = let val (rails', (_, y')) = fold_map (fn rail => fn (y0, y') => if is_newline rail then (Newline (y' + 1), (y' + 1, y' + 2)) else let val (rail', y0') = vertical_range rail y0; in (rail', (y0, Int.max (y0', y'))) end) rails (y, y + 1) in (Cat (y, rails'), y') end and vertical_range (Bar cats) y = let val (cats', y') = fold_map vertical_range_cat cats y in (Bar cats', Int.max (y + 1, y')) end | vertical_range (Plus (cat1, cat2)) y = let val ([cat1', cat2'], y') = fold_map vertical_range_cat [cat1, cat2] y; in (Plus (cat1', cat2'), Int.max (y + 1, y')) end | vertical_range (Newline _) y = (Newline (y + 2), y + 3) | vertical_range atom y = (atom, y + 1); in fun output_rules ctxt rules = let val output_antiq = Antiquote.Antiq #> Document_Antiquotation.evaluate (single o Latex.symbols) ctxt #> Latex.output_text; fun output_text b s = Output.output s |> b ? enclose "\\isakeyword{" "}" |> enclose "\\isa{" "}"; fun output_cat c (Cat (_, rails)) = outputs c rails and outputs c [rail] = output c rail | outputs _ rails = implode (map (output "") rails) and output _ (Bar []) = "" | output c (Bar [cat]) = output_cat c cat | output _ (Bar (cat :: cats)) = "\\rail@bar\n" ^ output_cat "" cat ^ implode (map (fn Cat (y, rails) => "\\rail@nextbar{" ^ string_of_int y ^ "}\n" ^ outputs "" rails) cats) ^ "\\rail@endbar\n" | output c (Plus (cat, Cat (y, rails))) = "\\rail@plus\n" ^ output_cat c cat ^ "\\rail@nextplus{" ^ string_of_int y ^ "}\n" ^ outputs "c" rails ^ "\\rail@endplus\n" | output _ (Newline y) = "\\rail@cr{" ^ string_of_int y ^ "}\n" | output c (Nonterminal s) = "\\rail@" ^ c ^ "nont{" ^ output_text false s ^ "}[]\n" | output c (Terminal (b, s)) = "\\rail@" ^ c ^ "term{" ^ output_text b s ^ "}[]\n" | output c (Antiquote (b, a)) = "\\rail@" ^ c ^ (if b then "term{" else "nont{") ^ output_antiq a ^ "}[]\n"; fun output_rule (name, rail) = let val (rail', y') = vertical_range rail 0; val out_name = (case name of Antiquote.Text "" => "" | Antiquote.Text s => output_text false s | Antiquote.Antiq a => output_antiq a); in "\\rail@begin{" ^ string_of_int y' ^ "}{" ^ out_name ^ "}\n" ^ output "" rail' ^ "\\rail@end\n" end; in Latex.string (Latex.environment "railoutput" (implode (map output_rule rules))) end; val _ = Theory.setup (Thy_Output.antiquotation_raw_embedded \<^binding>\rail\ (Scan.lift Args.text_input) (fn ctxt => output_rules ctxt o read ctxt)); end; end;

", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\

code: 0x01d4ab group: letter \ code: 0x01d4ac group: letter \ code: 0x00211b group: letter \ code: 0x01d4ae group: letter \ code: 0x01d4af group: letter \ code: 0x01d4b0 group: letter \ code: 0x01d4b1 group: letter \ code: 0x01d4b2 group: letter \ code: 0x01d4b3 group: letter \ code: 0x01d4b4 group: letter \ code: 0x01d4b5 group: letter \ code: 0x01d5ba group: letter \ code: 0x01d5bb group: letter \ code: 0x01d5bc group: letter \ code: 0x01d5bd group: letter \ code: 0x01d5be group: letter \ code: 0x01d5bf group: letter \ code: 0x01d5c0 group: letter \ code: 0x01d5c1 group: letter \ code: 0x01d5c2 group: letter \ code: 0x01d5c3 group: letter \ code: 0x01d5c4 group: letter \ code: 0x01d5c5 group: letter \ code: 0x01d5c6 group: letter \ code: 0x01d5c7 group: letter \ code: 0x01d5c8 group: letter \