# HG changeset patch # User wenzelm # Date 1552173694 -3600 # Node ID b9985133805d117899bc26e2358121e2a8128506 # Parent 0cb8753bdb50a7c957786a5977e5b044df906be5 added semantic document markers; emulate old-style tags as "tag" markers, with subtle change of semantics for multiples tags (ever used?); tuned; diff -r 0cb8753bdb50 -r b9985133805d src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Sat Mar 09 23:57:07 2019 +0100 +++ b/src/Pure/General/symbol.scala Sun Mar 10 00:21:34 2019 +0100 @@ -493,6 +493,7 @@ /* 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) @@ -578,6 +579,14 @@ 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 = "\\" diff -r 0cb8753bdb50 -r b9985133805d src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Sat Mar 09 23:57:07 2019 +0100 +++ b/src/Pure/Isar/outer_syntax.ML Sun Mar 10 00:21:34 2019 +0100 @@ -185,20 +185,21 @@ Scan.ahead (before_command |-- Parse.position Parse.command) :|-- (fn (name, pos) => let val keywords = Thy_Header.get_keywords thy; - val command_tags = Parse.command -- Document_Source.tags; 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_tags |-- parse) >> (fn f => f tr0) + Parse.!!! (command_marker -- parse) >> (op |>) | SOME (Command {command_parser = Restricted_Parser parse, ...}) => before_command :|-- (fn restricted => - Parse.!!! (command_tags |-- parse restricted)) >> (fn f => f tr0) + Parse.!!! (command_marker -- parse restricted)) >> (op |>) | NONE => Scan.fail_with (fn _ => fn _ => let diff -r 0cb8753bdb50 -r b9985133805d src/Pure/Isar/parse.scala --- a/src/Pure/Isar/parse.scala Sat Mar 09 23:57:07 2019 +0100 +++ b/src/Pure/Isar/parse.scala Sun Mar 10 00:21:34 2019 +0100 @@ -80,7 +80,13 @@ tok.kind == Token.Kind.IDENT || tok.kind == Token.Kind.STRING) - def tags: Parser[List[String]] = rep($$$("%") ~> tag_name) + 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 annotation: Parser[Unit] = rep(marker | tag) ^^ { case _ => () } /* wrappers */ diff -r 0cb8753bdb50 -r b9985133805d src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Sat Mar 09 23:57:07 2019 +0100 +++ b/src/Pure/Isar/toplevel.ML Sun Mar 10 00:21:34 2019 +0100 @@ -37,6 +37,7 @@ val type_error: transition -> string val name: string -> transition -> transition val position: Position.T -> transition -> transition + val markers: Input.source list -> transition -> transition val timing: Time.time -> transition -> transition val init_theory: (unit -> theory) -> transition -> transition val is_init: transition -> bool @@ -85,6 +86,7 @@ val reset_theory: state -> state option val reset_proof: state -> state option val reset_notepad: state -> state option + val fork_presentation: transition -> transition * transition type result val join_results: result -> (transition * state) list val element_result: Keyword.keywords -> transition Thy_Element.element -> state -> result * state @@ -142,12 +144,9 @@ fun node_of (State ((node, _), _)) = node; fun previous_theory_of (State (_, prev_thy)) = prev_thy; -fun init_toplevel () = - let val thy0 = Theory.get_pure () handle Fail _ => Context.the_global_context (); - in State ((Toplevel, Proof_Context.init_global thy0), NONE) end; +fun init_toplevel () = State (node_presentation Toplevel, NONE); +fun theory_toplevel thy = State (node_presentation (Theory (Context.Theory thy)), NONE); -fun theory_toplevel thy = - State (node_presentation (Theory (Context.Theory thy)), NONE); fun level state = (case node_of state of @@ -289,22 +288,24 @@ local -fun apply_tr _ (Init f) (State ((Toplevel, _), _)) = - let val node = Theory (Context.Theory (Runtime.controlled_execution NONE f ())) - in State (node_presentation node, NONE) end - | apply_tr _ Exit (State ((node as Theory (Context.Theory thy), _), _)) = +fun apply_tr int trans state = + (case (trans, node_of state) of + (Init f, Toplevel) => + Runtime.controlled_execution NONE (fn () => + State (node_presentation (Theory (Context.Theory (f ()))), NONE)) () + | (Exit, node as Theory (Context.Theory thy)) => let val State ((node', pr_ctxt), _) = node |> apply_transaction (fn _ => node_presentation (Theory (Context.Theory (Theory.end_theory thy)))) (K ()); in State ((Toplevel, pr_ctxt), get_theory node') end - | apply_tr int (Keep f) state = - Runtime.controlled_execution (try generic_theory_of state) (fn x => tap (f int) x) state - | apply_tr _ (Transaction _) (State ((Toplevel, _), _)) = raise UNDEF - | apply_tr int (Transaction (f, g)) (State ((node, _), _)) = - apply_transaction (fn x => f int x) g node - | apply_tr _ _ _ = raise UNDEF; + | (Keep f, node) => + Runtime.controlled_execution (try generic_theory_of state) + (fn () => (f int state; State (node_presentation node, previous_theory_of state))) () + | (Transaction _, Toplevel) => raise UNDEF + | (Transaction (f, g), node) => apply_transaction (fn x => f int x) g node + | _ => raise UNDEF); fun apply_union _ [] state = raise FAILURE (state, UNDEF) | apply_union int (tr :: trs) state = @@ -314,9 +315,18 @@ | exn as FAILURE _ => raise exn | exn => raise FAILURE (state, exn); +fun apply_markers markers (state as State ((node, pr_ctxt), prev_thy)) = + let + val state' = + Runtime.controlled_execution (try generic_theory_of state) + (fn () => State ((node, fold Document_Marker.evaluate markers pr_ctxt), prev_thy)) (); + in (state', NONE) end + handle exn => (state, SOME exn); + in -fun apply_trans int trs state = (apply_union int trs state, NONE) +fun apply_trans int trans markers state = + (apply_union int trans state |> apply_markers markers) handle FAILURE (alt_state, exn) => (alt_state, SOME exn) | exn => (state, SOME exn); end; @@ -325,18 +335,19 @@ (* datatype transition *) datatype transition = Transition of - {name: string, (*command name*) - pos: Position.T, (*source position*) - timing: Time.time, (*prescient timing information*) - trans: trans list}; (*primitive transitions (union)*) + {name: string, (*command name*) + pos: Position.T, (*source position*) + markers: Input.source list, (*semantic document markers*) + timing: Time.time, (*prescient timing information*) + trans: trans list}; (*primitive transitions (union)*) -fun make_transition (name, pos, timing, trans) = - Transition {name = name, pos = pos, timing = timing, trans = trans}; +fun make_transition (name, pos, markers, timing, trans) = + Transition {name = name, pos = pos, markers = markers, timing = timing, trans = trans}; -fun map_transition f (Transition {name, pos, timing, trans}) = - make_transition (f (name, pos, timing, trans)); +fun map_transition f (Transition {name, pos, markers, timing, trans}) = + make_transition (f (name, pos, markers, timing, trans)); -val empty = make_transition ("", Position.none, Time.zeroTime, []); +val empty = make_transition ("", Position.none, [], Time.zeroTime, []); (* diagnostics *) @@ -355,20 +366,23 @@ (* modify transitions *) -fun name name = map_transition (fn (_, pos, timing, trans) => - (name, pos, timing, trans)); +fun name name = map_transition (fn (_, pos, markers, timing, trans) => + (name, pos, markers, timing, trans)); -fun position pos = map_transition (fn (name, _, timing, trans) => - (name, pos, timing, trans)); +fun position pos = map_transition (fn (name, _, markers, timing, trans) => + (name, pos, markers, timing, trans)); + +fun markers markers = map_transition (fn (name, pos, _, timing, trans) => + (name, pos, markers, timing, trans)); -fun timing timing = map_transition (fn (name, pos, _, trans) => - (name, pos, timing, trans)); +fun timing timing = map_transition (fn (name, pos, markers, _, trans) => + (name, pos, markers, timing, trans)); -fun add_trans tr = map_transition (fn (name, pos, timing, trans) => - (name, pos, timing, tr :: trans)); +fun add_trans tr = map_transition (fn (name, pos, markers, timing, trans) => + (name, pos, markers, timing, tr :: trans)); -val reset_trans = map_transition (fn (name, pos, timing, _) => - (name, pos, timing, [])); +val reset_trans = map_transition (fn (name, pos, markers, timing, _) => + (name, pos, markers, timing, [])); (* basic transitions *) @@ -605,9 +619,9 @@ local -fun app int (tr as Transition {trans, ...}) = +fun app int (tr as Transition {markers, trans, ...}) = setmp_thread_position tr - (Timing.protocol (name_of tr) (pos_of tr) (apply_trans int trans) + (Timing.protocol (name_of tr) (pos_of tr) (apply_trans int trans markers) ##> Option.map (fn UNDEF => ERROR (type_error tr) | exn => exn)); in @@ -707,18 +721,26 @@ then Future.proofs_enabled 1 else Future.proofs_enabled 2 orelse Future.proofs_enabled_timing estimate)); +val empty_markers = markers []; +val empty_trans = reset_trans #> keep (K ()); + +in + +fun fork_presentation tr = (tr |> empty_markers, tr |> empty_trans); + fun atom_result keywords tr st = let val st' = if Future.proofs_enabled 1 andalso Keyword.is_diag keywords (name_of tr) then - (Execution.fork - {name = "Toplevel.diag", pos = pos_of tr, pri = ~1} - (fn () => command tr st); st) + let + val (tr1, tr2) = fork_presentation tr; + val _ = + Execution.fork {name = "Toplevel.diag", pos = pos_of tr, pri = ~1} + (fn () => command tr1 st); + in command tr2 st end else command tr st; in (Result (tr, st'), st') end; -in - fun element_result keywords (Thy_Element.Element (tr, NONE)) st = atom_result keywords tr st | element_result keywords (elem as Thy_Element.Element (head_tr, SOME element_rest)) st = let @@ -734,6 +756,8 @@ in (Result_List (head_result :: proof_results), st'') end else let + val (end_tr1, end_tr2) = fork_presentation end_tr; + val finish = Context.Theory o Proof_Context.theory_of; val future_proof = @@ -744,10 +768,10 @@ let val State ((Proof (prf, (_, orig_gthy)), _), prev_thy) = st'; val node' = Proof (Proof_Node.apply (K state) prf, (finish, orig_gthy)); - val (result, result_state) = + val (results, result_state) = State (node_presentation node', prev_thy) - |> fold_map (element_result keywords) body_elems ||> command end_tr; - in (Result_List result, presentation_context0 result_state) end)) + |> fold_map (element_result keywords) body_elems ||> command end_tr1; + in (Result_List results, presentation_context0 result_state) end)) #> (fn (res, state') => state' |> put_result (Result_Future res)); val forked_proof = @@ -756,12 +780,12 @@ end_proof (fn _ => future_proof #> (fn state => state |> Proof.global_done_proof |> Result.put (get_result state))); - val st'' = st' - |> command (head_tr |> reset_trans |> forked_proof); - val end_result = Result (end_tr, st''); + val st'' = st' |> command (head_tr |> reset_trans |> forked_proof); + val end_st = st'' |> command end_tr2; + val end_result = Result (end_tr, end_st); val result = Result_List [head_result, Result.get (presentation_context0 st''), end_result]; - in (result, st'') end + in (result, end_st) end end; end; diff -r 0cb8753bdb50 -r b9985133805d src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Sat Mar 09 23:57:07 2019 +0100 +++ b/src/Pure/PIDE/command.ML Sun Mar 10 00:21:34 2019 +0100 @@ -217,8 +217,12 @@ fun run keywords int tr st = if Future.proofs_enabled 1 andalso Keyword.is_diag keywords (Toplevel.name_of tr) then - (Execution.fork {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1} - (fn () => Toplevel.command_exception int tr st); ([], SOME st)) + 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 = diff -r 0cb8753bdb50 -r b9985133805d src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Sat Mar 09 23:57:07 2019 +0100 +++ b/src/Pure/PIDE/command.scala Sun Mar 10 00:21:34 2019 +0100 @@ -475,6 +475,7 @@ 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 } diff -r 0cb8753bdb50 -r b9985133805d src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Sat Mar 09 23:57:07 2019 +0100 +++ b/src/Pure/PIDE/markup.ML Sun Mar 10 00:21:34 2019 +0100 @@ -32,6 +32,7 @@ val language_ML: bool -> T val language_SML: bool -> T val language_document: bool -> T + val language_document_marker: T val language_antiquotation: T val language_text: bool -> T val language_verbatim: bool -> T @@ -314,6 +315,8 @@ val language_ML = language' {name = "ML", symbols = false, antiquotes = true}; val language_SML = language' {name = "SML", symbols = false, antiquotes = false}; val language_document = language' {name = "document", symbols = false, antiquotes = true}; +val language_document_marker = + language {name = "document_marker", symbols = true, antiquotes = true, delimited = true}; val language_antiquotation = language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true}; val language_text = language' {name = "text", symbols = true, antiquotes = false}; diff -r 0cb8753bdb50 -r b9985133805d src/Pure/Pure.thy --- a/src/Pure/Pure.thy Sat Mar 09 23:57:07 2019 +0100 +++ b/src/Pure/Pure.thy Sun Mar 10 00:21:34 2019 +0100 @@ -7,7 +7,7 @@ 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" diff -r 0cb8753bdb50 -r b9985133805d src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Sat Mar 09 23:57:07 2019 +0100 +++ b/src/Pure/ROOT.ML Sun Mar 10 00:21:34 2019 +0100 @@ -208,6 +208,7 @@ ML_file "Isar/parse.ML"; ML_file "Thy/document_source.ML"; ML_file "Thy/thy_header.ML"; +ML_file "Thy/document_marker.ML"; (*proof context*) ML_file "Isar/object_logic.ML"; diff -r 0cb8753bdb50 -r b9985133805d src/Pure/Thy/document_marker.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Thy/document_marker.ML Sun Mar 10 00:21:34 2019 +0100 @@ -0,0 +1,64 @@ +(* 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 evaluate: Input.source -> marker +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; + + +(* 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 markers = + (case Token.read_body (Thy_Header.get_keywords' ctxt) (Parse.list parse_marker) syms of + SOME res => res + | NONE => error ("Bad input" ^ Position.here pos)); + in fold (fn src => #2 (check ctxt (Token.name_of_src src)) src) markers ctxt end; + + +(* concrete markers *) + +val _ = + Theory.setup + (setup (Binding.make ("tag", \<^here>)) (Scan.lift Parse.name) Document_Source.update_tags); + +end; diff -r 0cb8753bdb50 -r b9985133805d src/Pure/Thy/document_source.ML --- a/src/Pure/Thy/document_source.ML Sat Mar 09 23:57:07 2019 +0100 +++ b/src/Pure/Thy/document_source.ML Sun Mar 10 00:21:34 2019 +0100 @@ -14,8 +14,10 @@ val improper: Token.T list parser val improper_end: Token.T list parser val blank_end: Token.T list parser - val tag: string 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 end; structure Document_Source: DOCUMENT_SOURCE = @@ -41,11 +43,32 @@ val blank_end = Scan.repeat (Scan.unless space_proper (Scan.one Token.is_blank)); -(* tags *) +(* 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 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); + end; diff -r 0cb8753bdb50 -r b9985133805d src/Pure/Thy/thy_header.ML --- a/src/Pure/Thy/thy_header.ML Sat Mar 09 23:57:07 2019 +0100 +++ b/src/Pure/Thy/thy_header.ML Sun Mar 10 00:21:34 2019 +0100 @@ -175,10 +175,11 @@ Parse.command_name textN || Parse.command_name txtN || Parse.command_name text_rawN) -- - Document_Source.tags -- Parse.!!! Parse.document_source; + Document_Source.annotation -- Parse.!!! Parse.document_source; val parse_header = - (Scan.repeat heading -- Parse.command_name theoryN -- Document_Source.tags) |-- Parse.!!! args; + (Scan.repeat heading -- Parse.command_name theoryN -- Document_Source.annotation) + |-- Parse.!!! args; fun read_tokens pos toks = filter Token.is_proper toks diff -r 0cb8753bdb50 -r b9985133805d src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Sat Mar 09 23:57:07 2019 +0100 +++ b/src/Pure/Thy/thy_header.scala Sun Mar 10 00:21:34 2019 +0100 @@ -172,9 +172,9 @@ command(TEXT) | command(TXT) | command(TEXT_RAW)) ~ - tags ~! document_source + annotation ~! document_source - (rep(heading) ~ command(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x } + (rep(heading) ~ command(THEORY) ~ annotation) ~! args ^^ { case _ ~ x => x } } } diff -r 0cb8753bdb50 -r b9985133805d src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Sat Mar 09 23:57:07 2019 +0100 +++ b/src/Pure/Thy/thy_output.ML Sun Mar 10 00:21:34 2019 +0100 @@ -202,7 +202,7 @@ (* command spans *) -type command = string * Position.T * string list; (*name, position, tags*) +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; @@ -287,7 +287,8 @@ #> cons (Latex.string flag) | _ => I); - val Span ((cmd_name, cmd_pos, cmd_tags), srcs, span_newline) = span; + 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'} = @@ -371,19 +372,19 @@ Document_Source.improper |-- Parse.position (Scan.one (fn tok => Token.is_command tok andalso pred keywords (Token.content_of tok))) -- - Scan.repeat Document_Source.tag -- - Parse.!!!! ((Document_Source.improper -- locale -- Document_Source.improper) |-- - Parse.document_source --| Document_Source.improper_end) - >> (fn (((tok, pos'), tags), source) => - let val name = Token.content_of tok - in (SOME (name, pos', tags), (mk (name, source), (flag, d))) end)); + (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.tags - >> (fn ((cmd_mod, cmd), tags) => + 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, tags), + [(SOME (Token.content_of cmd, Token.pos_of cmd), (Basic_Token cmd, (markup_false, d)))])); val cmt = Scan.peek (fn d =>