merged
authorwenzelm
Sun Mar 10 21:33:05 2019 +0100 (6 weeks ago ago)
changeset 700741a7857abb75c
parent 70062 6a6cdf34e980
parent 70073 f752f3993db8
child 70075 2eade8651b93
merged
     1.1 --- a/Admin/components/components.sha1	Sun Mar 10 00:22:38 2019 +0000
     1.2 +++ b/Admin/components/components.sha1	Sun Mar 10 21:33:05 2019 +0100
     1.3 @@ -78,6 +78,7 @@
     1.4  bee32019e5d7cf096ef2ea1d836c732e9a7628cc  isabelle_fonts-20181124.tar.gz
     1.5  f249bc2c85bd2af9eee509de17187a766b74ab86  isabelle_fonts-20181129.tar.gz
     1.6  928b5320073d04d93bcc5bc4347b6d01632b9d45  isabelle_fonts-20190210.tar.gz
     1.7 +dfcdf9a757b9dc36cee87f82533b43c58ba84abe  isabelle_fonts-20190309.tar.gz
     1.8  0b2206f914336dec4923dd0479d8cee4b904f544  jdk-11+28.tar.gz
     1.9  3e05213cad47dbef52804fe329395db9b4e57f39  jdk-11.0.2+9.tar.gz
    1.10  71d19df63816e9be1c4c5eb44aea7a44cfadb319  jdk-11.tar.gz
     2.1 --- a/Admin/components/main	Sun Mar 10 00:22:38 2019 +0000
     2.2 +++ b/Admin/components/main	Sun Mar 10 21:33:05 2019 +0100
     2.3 @@ -4,7 +4,7 @@
     2.4  csdp-6.x
     2.5  cvc4-1.5-4
     2.6  e-2.0-2
     2.7 -isabelle_fonts-20190210
     2.8 +isabelle_fonts-20190309
     2.9  jdk-11.0.2+9
    2.10  jedit_build-20190224
    2.11  jfreechart-1.5.0
     3.1 --- a/etc/symbols	Sun Mar 10 00:22:38 2019 +0000
     3.2 +++ b/etc/symbols	Sun Mar 10 21:33:05 2019 +0100
     3.3 @@ -361,6 +361,7 @@
     3.4  \<comment>              code: 0x002015  group: document  argument: space_cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
     3.5  \<^cancel>              code: 0x002326  group: document  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
     3.6  \<^latex>                               group: document  argument: cartouche
     3.7 +\<^marker>              code: 0x002710  group: document  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
     3.8  \<open>                 code: 0x002039  group: punctuation  font: Isabelle␣DejaVu␣Sans␣Mono  abbrev: <<
     3.9  \<close>                code: 0x00203a  group: punctuation  font: Isabelle␣DejaVu␣Sans␣Mono  abbrev: >>
    3.10  \<^here>                code: 0x002302  font: Isabelle␣DejaVu␣Sans␣Mono
     4.1 --- a/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy	Sun Mar 10 00:22:38 2019 +0000
     4.2 +++ b/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy	Sun Mar 10 21:33:05 2019 +0100
     4.3 @@ -235,10 +235,12 @@
     4.4          with less.prems have "y \<noteq> 0" "z \<noteq> 0" by auto
     4.5          have normalized_factors_product:
     4.6            "{p. p dvd a * b \<and> normalize p = p} = 
     4.7 -             (\<lambda>(x,y). x * y) ` ({p. p dvd a \<and> normalize p = p} \<times> {p. p dvd b \<and> normalize p = p})" for a b
     4.8 +             (\<lambda>(x,y). x * y) ` ({p. p dvd a \<and> normalize p = p} \<times> {p. p dvd b \<and> normalize p = p})"
     4.9 +          for a b
    4.10          proof safe
    4.11            fix p assume p: "p dvd a * b" "normalize p = p"
    4.12 -          from dvd_productE[OF p(1)] guess x y . note xy = this
    4.13 +          from p(1) obtain x y where xy: "p = x * y" "x dvd a" "y dvd b"
    4.14 +            by (rule dvd_productE)
    4.15            define x' y' where "x' = normalize x" and "y' = normalize y"
    4.16            have "p = x' * y'"
    4.17              by (subst p(2) [symmetric]) (simp add: xy x'_def y'_def normalize_mult)
     5.1 --- a/src/Pure/Admin/build_fonts.scala	Sun Mar 10 00:22:38 2019 +0000
     5.2 +++ b/src/Pure/Admin/build_fonts.scala	Sun Mar 10 21:33:05 2019 +0100
     5.3 @@ -30,6 +30,7 @@
     5.4          0x203a,  // single guillemet
     5.5          0x204b,  // FOOTNOTE
     5.6          0x20ac,  // Euro
     5.7 +        0x2710,  // pencil
     5.8          0xfb01,  // ligature fi
     5.9          0xfb02,  // ligature fl
    5.10          0xfffd,  // replacement character
     6.1 --- a/src/Pure/General/antiquote.ML	Sun Mar 10 00:22:38 2019 +0000
     6.2 +++ b/src/Pure/General/antiquote.ML	Sun Mar 10 21:33:05 2019 +0100
     6.3 @@ -122,12 +122,12 @@
     6.4    scan_nl || Scan.repeats1 scan_plain_txt @@@ scan_nl_opt;
     6.5  
     6.6  val scan_text_comments =
     6.7 -  scan_nl || Scan.repeats1 (Comment.scan >> #2 || scan_plain_txt) @@@ scan_nl_opt;
     6.8 +  scan_nl || Scan.repeats1 (Comment.scan_inner >> #2 || scan_plain_txt) @@@ scan_nl_opt;
     6.9  
    6.10  val scan_antiq_body =
    6.11    Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 ||
    6.12    Symbol_Pos.scan_cartouche err_prefix ||
    6.13 -  Comment.scan --
    6.14 +  Comment.scan_inner --
    6.15      Symbol_Pos.!!! (fn () => err_prefix ^ "bad formal comment in antiquote body") Scan.fail
    6.16      >> K [] ||
    6.17    Scan.one (fn (s, _) => s <> "}" andalso Symbol.not_eof s) >> single;
     7.1 --- a/src/Pure/General/comment.ML	Sun Mar 10 00:22:38 2019 +0000
     7.2 +++ b/src/Pure/General/comment.ML	Sun Mar 10 21:33:05 2019 +0100
     7.3 @@ -6,13 +6,15 @@
     7.4  
     7.5  signature COMMENT =
     7.6  sig
     7.7 -  datatype kind = Comment | Cancel | Latex
     7.8 +  datatype kind = Comment | Cancel | Latex | Marker
     7.9    val markups: kind -> Markup.T list
    7.10    val is_symbol: Symbol.symbol -> bool
    7.11    val scan_comment: (kind * Symbol_Pos.T list) scanner
    7.12    val scan_cancel: (kind * Symbol_Pos.T list) scanner
    7.13    val scan_latex: (kind * Symbol_Pos.T list) scanner
    7.14 -  val scan: (kind * Symbol_Pos.T list) scanner
    7.15 +  val scan_marker: (kind * Symbol_Pos.T list) scanner
    7.16 +  val scan_inner: (kind * Symbol_Pos.T list) scanner
    7.17 +  val scan_outer: (kind * Symbol_Pos.T list) scanner
    7.18    val read_body: Symbol_Pos.T list -> (kind option * Symbol_Pos.T list) list
    7.19  end;
    7.20  
    7.21 @@ -21,7 +23,7 @@
    7.22  
    7.23  (* kinds *)
    7.24  
    7.25 -datatype kind = Comment | Cancel | Latex;
    7.26 +datatype kind = Comment | Cancel | Latex | Marker;
    7.27  
    7.28  val kinds =
    7.29    [(Comment,
    7.30 @@ -32,7 +34,10 @@
    7.31        markups = [Markup.language_text true]}),
    7.32     (Latex,
    7.33       {symbol = Symbol.latex, blanks = false,
    7.34 -      markups = [Markup.language_latex true, Markup.no_words]})];
    7.35 +      markups = [Markup.language_latex true, Markup.no_words]}),
    7.36 +   (Marker,
    7.37 +     {symbol = Symbol.marker, blanks = false,
    7.38 +      markups = [Markup.language_document_marker]})];
    7.39  
    7.40  val get_kind = the o AList.lookup (op =) kinds;
    7.41  val print_kind = quote o #symbol o get_kind;
    7.42 @@ -69,7 +74,10 @@
    7.43  val scan_comment = scan_strict Comment;
    7.44  val scan_cancel = scan_strict Cancel;
    7.45  val scan_latex = scan_strict Latex;
    7.46 -val scan = scan_comment || scan_cancel || scan_latex;
    7.47 +val scan_marker = scan_strict Marker;
    7.48 +
    7.49 +val scan_inner = scan_comment || scan_cancel || scan_latex;
    7.50 +val scan_outer = scan_inner || scan_marker;
    7.51  
    7.52  val scan_body =
    7.53    Scan.many1 (fn (s, _) => not (is_symbol s) andalso Symbol.not_eof s) >> pair NONE ||
     8.1 --- a/src/Pure/General/comment.scala	Sun Mar 10 00:22:38 2019 +0000
     8.2 +++ b/src/Pure/General/comment.scala	Sun Mar 10 21:33:05 2019 +0100
     8.3 @@ -14,12 +14,14 @@
     8.4      val COMMENT = Value("formal comment")
     8.5      val CANCEL = Value("canceled text")
     8.6      val LATEX = Value("embedded LaTeX")
     8.7 +    val MARKER = Value("document marker")
     8.8    }
     8.9  
    8.10    lazy val symbols: Set[Symbol.Symbol] =
    8.11      Set(Symbol.comment, Symbol.comment_decoded,
    8.12        Symbol.cancel, Symbol.cancel_decoded,
    8.13 -      Symbol.latex, Symbol.latex_decoded)
    8.14 +      Symbol.latex, Symbol.latex_decoded,
    8.15 +      Symbol.marker, Symbol.marker_decoded)
    8.16  
    8.17    lazy val symbols_blanks: Set[Symbol.Symbol] =
    8.18      Set(Symbol.comment, Symbol.comment_decoded)
     9.1 --- a/src/Pure/General/symbol.ML	Sun Mar 10 00:22:38 2019 +0000
     9.2 +++ b/src/Pure/General/symbol.ML	Sun Mar 10 21:33:05 2019 +0100
     9.3 @@ -18,6 +18,7 @@
     9.4    val comment: symbol
     9.5    val cancel: symbol
     9.6    val latex: symbol
     9.7 +  val marker: symbol
     9.8    val is_char: symbol -> bool
     9.9    val is_utf8: symbol -> bool
    9.10    val is_symbolic: symbol -> bool
    9.11 @@ -120,6 +121,7 @@
    9.12  val comment = "\<comment>";
    9.13  val cancel = "\<^cancel>";
    9.14  val latex = "\<^latex>";
    9.15 +val marker = "\<^marker>";
    9.16  
    9.17  fun is_char s = size s = 1;
    9.18  
    10.1 --- a/src/Pure/General/symbol.scala	Sun Mar 10 00:22:38 2019 +0000
    10.2 +++ b/src/Pure/General/symbol.scala	Sun Mar 10 21:33:05 2019 +0100
    10.3 @@ -496,6 +496,7 @@
    10.4      val comment_decoded = decode(comment)
    10.5      val cancel_decoded = decode(cancel)
    10.6      val latex_decoded = decode(latex)
    10.7 +    val marker_decoded = decode(marker)
    10.8      val open_decoded = decode(open)
    10.9      val close_decoded = decode(close)
   10.10  
   10.11 @@ -583,10 +584,12 @@
   10.12    val comment: Symbol = "\\<comment>"
   10.13    val cancel: Symbol = "\\<^cancel>"
   10.14    val latex: Symbol = "\\<^latex>"
   10.15 +  val marker: Symbol = "\\<^marker>"
   10.16  
   10.17    def comment_decoded: Symbol = symbols.comment_decoded
   10.18    def cancel_decoded: Symbol = symbols.cancel_decoded
   10.19    def latex_decoded: Symbol = symbols.latex_decoded
   10.20 +  def marker_decoded: Symbol = symbols.marker_decoded
   10.21  
   10.22  
   10.23    /* cartouches */
    11.1 --- a/src/Pure/Isar/isar_cmd.ML	Sun Mar 10 00:22:38 2019 +0000
    11.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sun Mar 10 21:33:05 2019 +0100
    11.3 @@ -180,19 +180,23 @@
    11.4  
    11.5  structure Diag_State = Proof_Data
    11.6  (
    11.7 -  type T = Toplevel.state;
    11.8 -  fun init _ = Toplevel.toplevel;
    11.9 +  type T = Toplevel.state option;
   11.10 +  fun init _ = NONE;
   11.11  );
   11.12  
   11.13  fun ml_diag verbose source = Toplevel.keep (fn state =>
   11.14    let
   11.15      val opt_ctxt =
   11.16        try Toplevel.generic_theory_of state
   11.17 -      |> Option.map (Context.proof_of #> Diag_State.put state);
   11.18 +      |> Option.map (Context.proof_of #> Diag_State.put (SOME state));
   11.19      val flags = ML_Compiler.verbose verbose ML_Compiler.flags;
   11.20    in ML_Context.eval_source_in opt_ctxt flags source end);
   11.21  
   11.22 -val diag_state = Diag_State.get;
   11.23 +fun diag_state ctxt =
   11.24 +  (case Diag_State.get ctxt of
   11.25 +    SOME st => st
   11.26 +  | NONE => Toplevel.init_toplevel ());
   11.27 +
   11.28  val diag_goal = Proof.goal o Toplevel.proof_of o diag_state;
   11.29  
   11.30  val _ = Theory.setup
    12.1 --- a/src/Pure/Isar/outer_syntax.ML	Sun Mar 10 00:22:38 2019 +0000
    12.2 +++ b/src/Pure/Isar/outer_syntax.ML	Sun Mar 10 21:33:05 2019 +0100
    12.3 @@ -22,10 +22,10 @@
    12.4    val local_theory_to_proof: command_keyword -> string ->
    12.5      (local_theory -> Proof.state) parser -> unit
    12.6    val bootstrap: bool Config.T
    12.7 -  val parse_tokens: theory -> Token.T list -> Toplevel.transition list
    12.8 -  val parse: theory -> Position.T -> string -> Toplevel.transition list
    12.9    val parse_spans: Token.T list -> Command_Span.span list
   12.10    val make_span: Token.T list -> Command_Span.span
   12.11 +  val parse_span: theory -> (unit -> theory) -> Token.T list -> Toplevel.transition
   12.12 +  val parse_text: theory -> (unit -> theory) -> Position.T -> string -> Toplevel.transition list
   12.13    val command_reports: theory -> Token.T -> Position.report_text list
   12.14    val check_command: Proof.context -> command_keyword -> string
   12.15  end;
   12.16 @@ -172,59 +172,6 @@
   12.17  
   12.18  (** toplevel parsing **)
   12.19  
   12.20 -(* parse commands *)
   12.21 -
   12.22 -val bootstrap = Config.declare_bool ("Outer_Syntax.bootstrap", \<^here>) (K true);
   12.23 -
   12.24 -local
   12.25 -
   12.26 -val before_command =
   12.27 -  Scan.option (Parse.position (Parse.private >> K true || Parse.qualified >> K false));
   12.28 -
   12.29 -fun parse_command thy =
   12.30 -  Scan.ahead (before_command |-- Parse.position Parse.command) :|-- (fn (name, pos) =>
   12.31 -    let
   12.32 -      val keywords = Thy_Header.get_keywords thy;
   12.33 -      val command_tags = Parse.command -- Document_Source.tags;
   12.34 -      val tr0 =
   12.35 -        Toplevel.empty
   12.36 -        |> Toplevel.name name
   12.37 -        |> Toplevel.position pos
   12.38 -        |> Keyword.is_proof_open keywords name ? Toplevel.skip_proof_open
   12.39 -        |> Keyword.is_proof_close keywords name ? Toplevel.skip_proof_close;
   12.40 -    in
   12.41 -      (case lookup_commands thy name of
   12.42 -        SOME (Command {command_parser = Parser parse, ...}) =>
   12.43 -          Parse.!!! (command_tags |-- parse) >> (fn f => f tr0)
   12.44 -      | SOME (Command {command_parser = Restricted_Parser parse, ...}) =>
   12.45 -          before_command :|-- (fn restricted =>
   12.46 -            Parse.!!! (command_tags |-- parse restricted)) >> (fn f => f tr0)
   12.47 -      | NONE =>
   12.48 -          Scan.fail_with (fn _ => fn _ =>
   12.49 -            let
   12.50 -              val msg =
   12.51 -                if Config.get_global thy bootstrap
   12.52 -                then "missing theory context for command "
   12.53 -                else "undefined command ";
   12.54 -            in msg ^ quote (Markup.markup Markup.keyword1 name) end))
   12.55 -    end);
   12.56 -
   12.57 -in
   12.58 -
   12.59 -fun parse_tokens thy =
   12.60 -  filter Token.is_proper
   12.61 -  #> Source.of_list
   12.62 -  #> Source.source Token.stopper (Scan.bulk (fn xs => Parse.!!! (parse_command thy) xs))
   12.63 -  #> Source.exhaust;
   12.64 -
   12.65 -fun parse thy pos text =
   12.66 -  Symbol_Pos.explode (text, pos)
   12.67 -  |> Token.tokenize (Thy_Header.get_keywords thy) {strict = false}
   12.68 -  |> parse_tokens thy;
   12.69 -
   12.70 -end;
   12.71 -
   12.72 -
   12.73  (* parse spans *)
   12.74  
   12.75  local
   12.76 @@ -266,6 +213,75 @@
   12.77    | _ => Command_Span.Span (Command_Span.Malformed_Span, toks));
   12.78  
   12.79  
   12.80 +(* parse commands *)
   12.81 +
   12.82 +val bootstrap = Config.declare_bool ("Outer_Syntax.bootstrap", \<^here>) (K true);
   12.83 +
   12.84 +local
   12.85 +
   12.86 +val before_command =
   12.87 +  Scan.option (Parse.position (Parse.private >> K true || Parse.qualified >> K false));
   12.88 +
   12.89 +fun parse_command thy markers =
   12.90 +  Scan.ahead (before_command |-- Parse.position Parse.command) :|-- (fn (name, pos) =>
   12.91 +    let
   12.92 +      val keywords = Thy_Header.get_keywords thy;
   12.93 +      val tr0 =
   12.94 +        Toplevel.empty
   12.95 +        |> Toplevel.name name
   12.96 +        |> Toplevel.position pos
   12.97 +        |> Keyword.is_proof_open keywords name ? Toplevel.skip_proof_open
   12.98 +        |> Keyword.is_proof_close keywords name ? Toplevel.skip_proof_close;
   12.99 +      val command_markers =
  12.100 +        Parse.command |-- Document_Source.tags >>
  12.101 +          (fn tags => Toplevel.markers (map Document_Marker.legacy_tag tags @ markers) tr0);
  12.102 +    in
  12.103 +      (case lookup_commands thy name of
  12.104 +        SOME (Command {command_parser = Parser parse, ...}) =>
  12.105 +          Parse.!!! (command_markers -- parse) >> (op |>)
  12.106 +      | SOME (Command {command_parser = Restricted_Parser parse, ...}) =>
  12.107 +          before_command :|-- (fn restricted =>
  12.108 +            Parse.!!! (command_markers -- parse restricted)) >> (op |>)
  12.109 +      | NONE =>
  12.110 +          Scan.fail_with (fn _ => fn _ =>
  12.111 +            let
  12.112 +              val msg =
  12.113 +                if Config.get_global thy bootstrap
  12.114 +                then "missing theory context for command "
  12.115 +                else "undefined command ";
  12.116 +            in msg ^ quote (Markup.markup Markup.keyword1 name) end))
  12.117 +    end);
  12.118 +
  12.119 +in
  12.120 +
  12.121 +fun parse_span thy init span =
  12.122 +  let
  12.123 +    val range = Token.range_of span;
  12.124 +    val core_range = Token.core_range_of span;
  12.125 +
  12.126 +    val markers = map Token.input_of (filter Token.is_document_marker span);
  12.127 +    fun parse () =
  12.128 +      filter Token.is_proper span
  12.129 +      |> Source.of_list
  12.130 +      |> Source.source Token.stopper (Scan.bulk (fn xs => Parse.!!! (parse_command thy markers) xs))
  12.131 +      |> Source.exhaust;
  12.132 +  in
  12.133 +    (case parse () of
  12.134 +      [tr] => Toplevel.modify_init init tr
  12.135 +    | [] => Toplevel.ignored (#1 range)
  12.136 +    | _ => Toplevel.malformed (#1 core_range) "Exactly one command expected")
  12.137 +    handle ERROR msg => Toplevel.malformed (#1 core_range) msg
  12.138 +  end;
  12.139 +
  12.140 +fun parse_text thy init pos text =
  12.141 +  Symbol_Pos.explode (text, pos)
  12.142 +  |> Token.tokenize (Thy_Header.get_keywords thy) {strict = false}
  12.143 +  |> parse_spans
  12.144 +  |> map (Command_Span.content #> parse_span thy init);
  12.145 +
  12.146 +end;
  12.147 +
  12.148 +
  12.149  (* check commands *)
  12.150  
  12.151  fun command_reports thy tok =
    13.1 --- a/src/Pure/Isar/parse.ML	Sun Mar 10 00:22:38 2019 +0000
    13.2 +++ b/src/Pure/Isar/parse.ML	Sun Mar 10 21:33:05 2019 +0100
    13.3 @@ -96,6 +96,7 @@
    13.4    val for_fixes: (binding * string option * mixfix) list parser
    13.5    val ML_source: Input.source parser
    13.6    val document_source: Input.source parser
    13.7 +  val document_marker: Input.source parser
    13.8    val const: string parser
    13.9    val term: string parser
   13.10    val prop: string parser
   13.11 @@ -390,6 +391,10 @@
   13.12  val ML_source = input (group (fn () => "ML source") text);
   13.13  val document_source = input (group (fn () => "document source") text);
   13.14  
   13.15 +val document_marker =
   13.16 +  group (fn () => "document marker")
   13.17 +    (RESET_VALUE (Scan.one Token.is_document_marker >> Token.input_of));
   13.18 +
   13.19  
   13.20  (* terms *)
   13.21  
    14.1 --- a/src/Pure/Isar/parse.scala	Sun Mar 10 00:22:38 2019 +0000
    14.2 +++ b/src/Pure/Isar/parse.scala	Sun Mar 10 21:33:05 2019 +0100
    14.3 @@ -80,7 +80,12 @@
    14.4            tok.kind == Token.Kind.IDENT ||
    14.5            tok.kind == Token.Kind.STRING)
    14.6  
    14.7 -    def tags: Parser[List[String]] = rep($$$("%") ~> tag_name)
    14.8 +    def tag: Parser[String] = $$$("%") ~> tag_name
    14.9 +    def tags: Parser[List[String]] = rep(tag)
   14.10 +
   14.11 +    def marker: Parser[String] = token("marker", _.is_marker) ^^ (_.content)
   14.12 +
   14.13 +    def annotation: Parser[Unit] = rep(tag | marker) ^^ { case _ => () }
   14.14  
   14.15  
   14.16      /* wrappers */
    15.1 --- a/src/Pure/Isar/token.ML	Sun Mar 10 00:22:38 2019 +0000
    15.2 +++ b/src/Pure/Isar/token.ML	Sun Mar 10 21:33:05 2019 +0100
    15.3 @@ -30,7 +30,6 @@
    15.4      Declaration of declaration |
    15.5      Files of file Exn.result list
    15.6    val pos_of: T -> Position.T
    15.7 -  val range_of: T list -> Position.range
    15.8    val adjust_offsets: (int -> int option) -> T -> T
    15.9    val eof: T
   15.10    val is_eof: T -> bool
   15.11 @@ -46,6 +45,7 @@
   15.12    val is_comment: T -> bool
   15.13    val is_informal_comment: T -> bool
   15.14    val is_formal_comment: T -> bool
   15.15 +  val is_document_marker: T -> bool
   15.16    val is_ignored: T -> bool
   15.17    val is_begin_ignore: T -> bool
   15.18    val is_end_ignore: T -> bool
   15.19 @@ -53,6 +53,8 @@
   15.20    val is_space: T -> bool
   15.21    val is_blank: T -> bool
   15.22    val is_newline: T -> bool
   15.23 +  val range_of: T list -> Position.range
   15.24 +  val core_range_of: T list -> Position.range
   15.25    val content_of: T -> string
   15.26    val source_of: T -> string
   15.27    val input_of: T -> Input.source
   15.28 @@ -190,11 +192,6 @@
   15.29  fun pos_of (Token ((_, (pos, _)), _, _)) = pos;
   15.30  fun end_pos_of (Token ((_, (_, pos)), _, _)) = pos;
   15.31  
   15.32 -fun range_of (toks as tok :: _) =
   15.33 -      let val pos' = end_pos_of (List.last toks)
   15.34 -      in Position.range (pos_of tok, pos') end
   15.35 -  | range_of [] = Position.no_range;
   15.36 -
   15.37  fun adjust_offsets adjust (Token ((x, range), y, z)) =
   15.38    Token ((x, apply2 (Position.adjust_offsets adjust) range), y, z);
   15.39  
   15.40 @@ -245,6 +242,9 @@
   15.41  fun is_formal_comment (Token (_, (Comment (SOME _), _), _)) = true
   15.42    | is_formal_comment _ = false;
   15.43  
   15.44 +fun is_document_marker (Token (_, (Comment (SOME Comment.Marker), _), _)) = true
   15.45 +  | is_document_marker _ = false;
   15.46 +
   15.47  fun is_begin_ignore (Token (_, (Comment NONE, "<"), _)) = true
   15.48    | is_begin_ignore _ = false;
   15.49  
   15.50 @@ -267,6 +267,17 @@
   15.51    | is_newline _ = false;
   15.52  
   15.53  
   15.54 +(* range of tokens *)
   15.55 +
   15.56 +fun range_of (toks as tok :: _) =
   15.57 +      let val pos' = end_pos_of (List.last toks)
   15.58 +      in Position.range (pos_of tok, pos') end
   15.59 +  | range_of [] = Position.no_range;
   15.60 +
   15.61 +val core_range_of =
   15.62 +  drop_prefix is_ignored #> drop_suffix is_ignored #> range_of;
   15.63 +
   15.64 +
   15.65  (* token content *)
   15.66  
   15.67  fun content_of (Token (_, (_, x), _)) = x;
   15.68 @@ -636,7 +647,7 @@
   15.69      scan_verbatim >> token_range Verbatim ||
   15.70      scan_cartouche >> token_range Cartouche ||
   15.71      scan_comment >> token_range (Comment NONE) ||
   15.72 -    Comment.scan >> (fn (k, ss) => token (Comment (SOME k)) ss) ||
   15.73 +    Comment.scan_outer >> (fn (k, ss) => token (Comment (SOME k)) ss) ||
   15.74      scan_space >> token Space ||
   15.75      (Scan.max token_leq
   15.76        (Scan.max token_leq
    16.1 --- a/src/Pure/Isar/token.scala	Sun Mar 10 00:22:38 2019 +0000
    16.2 +++ b/src/Pure/Isar/token.scala	Sun Mar 10 21:33:05 2019 +0100
    16.3 @@ -304,6 +304,9 @@
    16.4    def is_space: Boolean = kind == Token.Kind.SPACE
    16.5    def is_informal_comment: Boolean = kind == Token.Kind.INFORMAL_COMMENT
    16.6    def is_formal_comment: Boolean = kind == Token.Kind.FORMAL_COMMENT
    16.7 +  def is_marker: Boolean =
    16.8 +    kind == Token.Kind.FORMAL_COMMENT &&
    16.9 +    (source.startsWith(Symbol.marker) || source.startsWith(Symbol.marker_decoded))
   16.10    def is_comment: Boolean = is_informal_comment || is_formal_comment
   16.11    def is_ignored: Boolean = is_space || is_informal_comment
   16.12    def is_proper: Boolean = !is_space && !is_comment
    17.1 --- a/src/Pure/Isar/toplevel.ML	Sun Mar 10 00:22:38 2019 +0000
    17.2 +++ b/src/Pure/Isar/toplevel.ML	Sun Mar 10 21:33:05 2019 +0100
    17.3 @@ -8,8 +8,8 @@
    17.4  sig
    17.5    exception UNDEF
    17.6    type state
    17.7 +  val init_toplevel: unit -> state
    17.8    val theory_toplevel: theory -> state
    17.9 -  val toplevel: state
   17.10    val is_toplevel: state -> bool
   17.11    val is_theory: state -> bool
   17.12    val is_proof: state -> bool
   17.13 @@ -37,6 +37,7 @@
   17.14    val type_error: transition -> string
   17.15    val name: string -> transition -> transition
   17.16    val position: Position.T -> transition -> transition
   17.17 +  val markers: Input.source list -> transition -> transition
   17.18    val timing: Time.time -> transition -> transition
   17.19    val init_theory: (unit -> theory) -> transition -> transition
   17.20    val is_init: transition -> bool
   17.21 @@ -85,6 +86,7 @@
   17.22    val reset_theory: state -> state option
   17.23    val reset_proof: state -> state option
   17.24    val reset_notepad: state -> state option
   17.25 +  val fork_presentation: transition -> transition * transition
   17.26    type result
   17.27    val join_results: result -> (transition * state) list
   17.28    val element_result: Keyword.keywords -> transition Thy_Element.element -> state -> result * state
   17.29 @@ -101,6 +103,8 @@
   17.30  (* datatype node *)
   17.31  
   17.32  datatype node =
   17.33 +  Toplevel
   17.34 +    (*toplevel outside of theory body*) |
   17.35    Theory of generic_theory
   17.36      (*global or local theory*) |
   17.37    Proof of Proof_Node.T * ((Proof.context -> generic_theory) * generic_theory)
   17.38 @@ -112,68 +116,87 @@
   17.39  val proof_node = fn Proof (prf, _) => SOME prf | _ => NONE;
   17.40  val skipped_proof_node = fn Skipped_Proof _ => true | _ => false;
   17.41  
   17.42 -fun cases_node f _ (Theory gthy) = f gthy
   17.43 -  | cases_node _ g (Proof (prf, _)) = g (Proof_Node.current prf)
   17.44 -  | cases_node f _ (Skipped_Proof (_, (gthy, _))) = f gthy;
   17.45 +fun cases_node f _ _ Toplevel = f ()
   17.46 +  | cases_node _ g _ (Theory gthy) = g gthy
   17.47 +  | cases_node _ _ h (Proof (prf, _)) = h (Proof_Node.current prf)
   17.48 +  | cases_node _ g _ (Skipped_Proof (_, (gthy, _))) = g gthy;
   17.49 +
   17.50 +fun cases_proper_node g h = cases_node (fn () => raise UNDEF) g h;
   17.51 +
   17.52 +val get_theory = cases_node (K NONE) (SOME o Context.theory_of) (SOME o Proof.theory_of);
   17.53  
   17.54  
   17.55  (* datatype state *)
   17.56  
   17.57 -type node_presentation = node * Proof.context;  (*node with presentation context*)
   17.58 -fun node_presentation0 node = (node, cases_node Context.proof_of Proof.context_of node);
   17.59 +type node_presentation = node * Proof.context;
   17.60  
   17.61 -datatype state = State of node_presentation option * node_presentation option; (*current, previous*)
   17.62 +fun init_presentation () =
   17.63 +  Proof_Context.init_global (Theory.get_pure_bootstrap ());
   17.64 +
   17.65 +fun node_presentation node =
   17.66 +  (node, cases_node init_presentation Context.proof_of Proof.context_of node);
   17.67 +
   17.68  
   17.69 -fun theory_toplevel thy = State (SOME (node_presentation0 (Theory (Context.Theory thy))), NONE);
   17.70 +datatype state =
   17.71 +  State of node_presentation * theory option;
   17.72 +    (*current node with presentation context, previous theory*)
   17.73  
   17.74 -val toplevel = State (NONE, NONE);
   17.75 +fun node_of (State ((node, _), _)) = node;
   17.76 +fun previous_theory_of (State (_, prev_thy)) = prev_thy;
   17.77  
   17.78 -fun is_toplevel (State (NONE, _)) = true
   17.79 -  | is_toplevel _ = false;
   17.80 +fun init_toplevel () = State (node_presentation Toplevel, NONE);
   17.81 +fun theory_toplevel thy = State (node_presentation (Theory (Context.Theory thy)), NONE);
   17.82  
   17.83 -fun level (State (NONE, _)) = 0
   17.84 -  | level (State (SOME (Theory _, _), _)) = 0
   17.85 -  | level (State (SOME (Proof (prf, _), _), _)) = Proof.level (Proof_Node.current prf)
   17.86 -  | level (State (SOME (Skipped_Proof (d, _), _), _)) = d + 1;   (*different notion of proof depth!*)
   17.87 +
   17.88 +fun level state =
   17.89 +  (case node_of state of
   17.90 +    Toplevel => 0
   17.91 +  | Theory _ => 0
   17.92 +  | Proof (prf, _) => Proof.level (Proof_Node.current prf)
   17.93 +  | Skipped_Proof (d, _) => d + 1);   (*different notion of proof depth!*)
   17.94  
   17.95 -fun str_of_state (State (NONE, SOME (Theory (Context.Theory thy), _))) =
   17.96 -      "at top level, result theory " ^ quote (Context.theory_name thy)
   17.97 -  | str_of_state (State (NONE, _)) = "at top level"
   17.98 -  | str_of_state (State (SOME (Theory (Context.Theory _), _), _)) = "in theory mode"
   17.99 -  | str_of_state (State (SOME (Theory (Context.Proof _), _), _)) = "in local theory mode"
  17.100 -  | str_of_state (State (SOME (Proof _, _), _)) = "in proof mode"
  17.101 -  | str_of_state (State (SOME (Skipped_Proof _, _), _)) = "in skipped proof mode";
  17.102 +fun str_of_state state =
  17.103 +  (case node_of state of
  17.104 +    Toplevel =>
  17.105 +      (case previous_theory_of state of
  17.106 +        NONE => "at top level"
  17.107 +      | SOME thy => "at top level, result theory " ^ quote (Context.theory_name thy))
  17.108 +  | Theory (Context.Theory _) => "in theory mode"
  17.109 +  | Theory (Context.Proof _) => "in local theory mode"
  17.110 +  | Proof _ => "in proof mode"
  17.111 +  | Skipped_Proof _ => "in skipped proof mode");
  17.112  
  17.113  
  17.114  (* current node *)
  17.115  
  17.116 -fun node_of (State (NONE, _)) = raise UNDEF
  17.117 -  | node_of (State (SOME (node, _), _)) = node;
  17.118 +fun is_toplevel state = (case node_of state of Toplevel => true | _ => false);
  17.119  
  17.120 -fun is_theory state = not (is_toplevel state) andalso is_some (theory_node (node_of state));
  17.121 -fun is_proof state = not (is_toplevel state) andalso is_some (proof_node (node_of state));
  17.122 -fun is_skipped_proof state = not (is_toplevel state) andalso skipped_proof_node (node_of state);
  17.123 +fun is_theory state =
  17.124 +  not (is_toplevel state) andalso is_some (theory_node (node_of state));
  17.125  
  17.126 -fun node_case f g state = cases_node f g (node_of state);
  17.127 +fun is_proof state =
  17.128 +  not (is_toplevel state) andalso is_some (proof_node (node_of state));
  17.129  
  17.130 -fun previous_theory_of (State (_, NONE)) = NONE
  17.131 -  | previous_theory_of (State (_, SOME (prev, _))) =
  17.132 -      SOME (cases_node Context.theory_of Proof.theory_of prev);
  17.133 +fun is_skipped_proof state =
  17.134 +  not (is_toplevel state) andalso skipped_proof_node (node_of state);
  17.135  
  17.136 -val context_of = node_case Context.proof_of Proof.context_of;
  17.137 -val generic_theory_of = node_case I (Context.Proof o Proof.context_of);
  17.138 -val theory_of = node_case Context.theory_of Proof.theory_of;
  17.139 -val proof_of = node_case (fn _ => error "No proof state") I;
  17.140 +fun proper_node_of state = if is_toplevel state then raise UNDEF else node_of state;
  17.141 +fun proper_node_case f g state = cases_proper_node f g (proper_node_of state);
  17.142 +
  17.143 +val context_of = proper_node_case Context.proof_of Proof.context_of;
  17.144 +val generic_theory_of = proper_node_case I (Context.Proof o Proof.context_of);
  17.145 +val theory_of = proper_node_case Context.theory_of Proof.theory_of;
  17.146 +val proof_of = proper_node_case (fn _ => error "No proof state") I;
  17.147  
  17.148  fun proof_position_of state =
  17.149 -  (case node_of state of
  17.150 +  (case proper_node_of state of
  17.151      Proof (prf, _) => Proof_Node.position prf
  17.152    | _ => ~1);
  17.153  
  17.154 -fun is_end_theory (State (NONE, SOME (Theory (Context.Theory _), _))) = true
  17.155 +fun is_end_theory (State ((Toplevel, _), SOME _)) = true
  17.156    | is_end_theory _ = false;
  17.157  
  17.158 -fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy), _))) = thy
  17.159 +fun end_theory _ (State ((Toplevel, _), SOME thy)) = thy
  17.160    | end_theory pos _ = error ("Malformed theory" ^ Position.here pos);
  17.161  
  17.162  
  17.163 @@ -185,13 +208,7 @@
  17.164    fun init _ = NONE;
  17.165  );
  17.166  
  17.167 -fun presentation_context0 state =
  17.168 -  (case state of
  17.169 -    State (SOME (_, ctxt), _) => ctxt
  17.170 -  | State (NONE, _) =>
  17.171 -      (case try Theory.get_pure () of
  17.172 -        SOME thy => Proof_Context.init_global thy
  17.173 -      | NONE => raise UNDEF));
  17.174 +fun presentation_context0 (State ((_, pr_ctxt), _)) = pr_ctxt;
  17.175  
  17.176  fun presentation_context (state as State (current, _)) =
  17.177    presentation_context0 state
  17.178 @@ -199,31 +216,31 @@
  17.179  
  17.180  fun presentation_state ctxt =
  17.181    (case Presentation_State.get ctxt of
  17.182 -    NONE => State (SOME (node_presentation0 (Theory (Context.Proof ctxt))), NONE)
  17.183 +    NONE => State (node_presentation (Theory (Context.Proof ctxt)), NONE)
  17.184    | SOME state => state);
  17.185  
  17.186  
  17.187  (* print state *)
  17.188  
  17.189  fun pretty_context state =
  17.190 -  (case try node_of state of
  17.191 -    NONE => []
  17.192 -  | SOME node =>
  17.193 -      let
  17.194 -        val gthy =
  17.195 -          (case node of
  17.196 -            Theory gthy => gthy
  17.197 -          | Proof (_, (_, gthy)) => gthy
  17.198 -          | Skipped_Proof (_, (_, gthy)) => gthy);
  17.199 -        val lthy = Context.cases Named_Target.theory_init I gthy;
  17.200 -      in Local_Theory.pretty lthy end);
  17.201 +  if is_toplevel state then []
  17.202 +  else
  17.203 +    let
  17.204 +      val gthy =
  17.205 +        (case node_of state of
  17.206 +          Toplevel => raise Match
  17.207 +        | Theory gthy => gthy
  17.208 +        | Proof (_, (_, gthy)) => gthy
  17.209 +        | Skipped_Proof (_, (_, gthy)) => gthy);
  17.210 +      val lthy = Context.cases Named_Target.theory_init I gthy;
  17.211 +    in Local_Theory.pretty lthy end;
  17.212  
  17.213  fun pretty_state state =
  17.214 -  (case try node_of state of
  17.215 -    NONE => []
  17.216 -  | SOME (Theory _) => []
  17.217 -  | SOME (Proof (prf, _)) => Proof.pretty_state (Proof_Node.current prf)
  17.218 -  | SOME (Skipped_Proof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]);
  17.219 +  (case node_of state of
  17.220 +    Toplevel => []
  17.221 +  | Theory _ => []
  17.222 +  | Proof (prf, _) => Proof.pretty_state (Proof_Node.current prf)
  17.223 +  | Skipped_Proof (d, _) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]);
  17.224  
  17.225  val string_of_state = pretty_state #> Pretty.chunks #> Pretty.string_of;
  17.226  
  17.227 @@ -235,35 +252,6 @@
  17.228  
  17.229  (** toplevel transitions **)
  17.230  
  17.231 -(* node transactions -- maintaining stable checkpoints *)
  17.232 -
  17.233 -exception FAILURE of state * exn;
  17.234 -
  17.235 -fun apply_transaction f g node =
  17.236 -  let
  17.237 -    val node_pr = node_presentation0 node;
  17.238 -    val context = cases_node I (Context.Proof o Proof.context_of) node;
  17.239 -    fun state_error e node_pr' = (State (SOME node_pr', SOME node_pr), e);
  17.240 -
  17.241 -    val (result, err) =
  17.242 -      node
  17.243 -      |> Runtime.controlled_execution (SOME context) f
  17.244 -      |> state_error NONE
  17.245 -      handle exn => state_error (SOME exn) node_pr;
  17.246 -  in
  17.247 -    (case err of
  17.248 -      NONE => tap g result
  17.249 -    | SOME exn => raise FAILURE (result, exn))
  17.250 -  end;
  17.251 -
  17.252 -val exit_transaction =
  17.253 -  apply_transaction
  17.254 -    ((fn Theory (Context.Theory thy) => Theory (Context.Theory (Theory.end_theory thy))
  17.255 -       | node => node) #> node_presentation0)
  17.256 -    (K ())
  17.257 -  #> (fn State (node_pr', _) => State (NONE, node_pr'));
  17.258 -
  17.259 -
  17.260  (* primitive transitions *)
  17.261  
  17.262  datatype trans =
  17.263 @@ -278,16 +266,43 @@
  17.264  
  17.265  local
  17.266  
  17.267 -fun apply_tr _ (Init f) (State (NONE, _)) =
  17.268 -      let val node = Theory (Context.Theory (Runtime.controlled_execution NONE f ()))
  17.269 -      in State (SOME (node_presentation0 node), NONE) end
  17.270 -  | apply_tr _ Exit (State (SOME (node as Theory (Context.Theory _), _), _)) =
  17.271 -      exit_transaction node
  17.272 -  | apply_tr int (Keep f) state =
  17.273 -      Runtime.controlled_execution (try generic_theory_of state) (fn x => tap (f int) x) state
  17.274 -  | apply_tr int (Transaction (f, g)) (State (SOME (node, _), _)) =
  17.275 -      apply_transaction (fn x => f int x) g node
  17.276 -  | apply_tr _ _ _ = raise UNDEF;
  17.277 +exception FAILURE of state * exn;
  17.278 +
  17.279 +fun apply f g node =
  17.280 +  let
  17.281 +    val node_pr = node_presentation node;
  17.282 +    val context = cases_proper_node I (Context.Proof o Proof.context_of) node;
  17.283 +    fun state_error e node_pr' = (State (node_pr', get_theory node), e);
  17.284 +
  17.285 +    val (result, err) =
  17.286 +      node
  17.287 +      |> Runtime.controlled_execution (SOME context) f
  17.288 +      |> state_error NONE
  17.289 +      handle exn => state_error (SOME exn) node_pr;
  17.290 +  in
  17.291 +    (case err of
  17.292 +      NONE => tap g result
  17.293 +    | SOME exn => raise FAILURE (result, exn))
  17.294 +  end;
  17.295 +
  17.296 +fun apply_tr int trans state =
  17.297 +  (case (trans, node_of state) of
  17.298 +    (Init f, Toplevel) =>
  17.299 +      Runtime.controlled_execution NONE (fn () =>
  17.300 +        State (node_presentation (Theory (Context.Theory (f ()))), NONE)) ()
  17.301 +  | (Exit, node as Theory (Context.Theory thy)) =>
  17.302 +      let
  17.303 +        val State ((node', pr_ctxt), _) =
  17.304 +          node |> apply
  17.305 +            (fn _ => node_presentation (Theory (Context.Theory (Theory.end_theory thy))))
  17.306 +            (K ());
  17.307 +      in State ((Toplevel, pr_ctxt), get_theory node') end
  17.308 +  | (Keep f, node) =>
  17.309 +      Runtime.controlled_execution (try generic_theory_of state)
  17.310 +        (fn () => (f int state; State (node_presentation node, previous_theory_of state))) ()
  17.311 +  | (Transaction _, Toplevel) => raise UNDEF
  17.312 +  | (Transaction (f, g), node) => apply (fn x => f int x) g node
  17.313 +  | _ => raise UNDEF);
  17.314  
  17.315  fun apply_union _ [] state = raise FAILURE (state, UNDEF)
  17.316    | apply_union int (tr :: trs) state =
  17.317 @@ -297,9 +312,18 @@
  17.318            | exn as FAILURE _ => raise exn
  17.319            | exn => raise FAILURE (state, exn);
  17.320  
  17.321 +fun apply_markers markers (state as State ((node, pr_ctxt), prev_thy)) =
  17.322 +  let
  17.323 +    val state' =
  17.324 +      Runtime.controlled_execution (try generic_theory_of state)
  17.325 +        (fn () => State ((node, fold Document_Marker.evaluate markers pr_ctxt), prev_thy)) ();
  17.326 +  in (state', NONE) end
  17.327 +  handle exn => (state, SOME exn);
  17.328 +
  17.329  in
  17.330  
  17.331 -fun apply_trans int trs state = (apply_union int trs state, NONE)
  17.332 +fun apply_trans int trans markers state =
  17.333 +  (apply_union int trans state |> apply_markers markers)
  17.334    handle FAILURE (alt_state, exn) => (alt_state, SOME exn) | exn => (state, SOME exn);
  17.335  
  17.336  end;
  17.337 @@ -308,18 +332,19 @@
  17.338  (* datatype transition *)
  17.339  
  17.340  datatype transition = Transition of
  17.341 - {name: string,              (*command name*)
  17.342 -  pos: Position.T,           (*source position*)
  17.343 -  timing: Time.time,         (*prescient timing information*)
  17.344 -  trans: trans list};        (*primitive transitions (union)*)
  17.345 + {name: string,               (*command name*)
  17.346 +  pos: Position.T,            (*source position*)
  17.347 +  markers: Input.source list, (*semantic document markers*)
  17.348 +  timing: Time.time,          (*prescient timing information*)
  17.349 +  trans: trans list};         (*primitive transitions (union)*)
  17.350  
  17.351 -fun make_transition (name, pos, timing, trans) =
  17.352 -  Transition {name = name, pos = pos, timing = timing, trans = trans};
  17.353 +fun make_transition (name, pos, markers, timing, trans) =
  17.354 +  Transition {name = name, pos = pos, markers = markers, timing = timing, trans = trans};
  17.355  
  17.356 -fun map_transition f (Transition {name, pos, timing, trans}) =
  17.357 -  make_transition (f (name, pos, timing, trans));
  17.358 +fun map_transition f (Transition {name, pos, markers, timing, trans}) =
  17.359 +  make_transition (f (name, pos, markers, timing, trans));
  17.360  
  17.361 -val empty = make_transition ("", Position.none, Time.zeroTime, []);
  17.362 +val empty = make_transition ("", Position.none, [], Time.zeroTime, []);
  17.363  
  17.364  
  17.365  (* diagnostics *)
  17.366 @@ -338,20 +363,23 @@
  17.367  
  17.368  (* modify transitions *)
  17.369  
  17.370 -fun name name = map_transition (fn (_, pos, timing, trans) =>
  17.371 -  (name, pos, timing, trans));
  17.372 +fun name name = map_transition (fn (_, pos, markers, timing, trans) =>
  17.373 +  (name, pos, markers, timing, trans));
  17.374  
  17.375 -fun position pos = map_transition (fn (name, _, timing, trans) =>
  17.376 -  (name, pos, timing, trans));
  17.377 +fun position pos = map_transition (fn (name, _, markers, timing, trans) =>
  17.378 +  (name, pos, markers, timing, trans));
  17.379 +
  17.380 +fun markers markers = map_transition (fn (name, pos, _, timing, trans) =>
  17.381 +  (name, pos, markers, timing, trans));
  17.382  
  17.383 -fun timing timing = map_transition (fn (name, pos, _, trans) =>
  17.384 -  (name, pos, timing, trans));
  17.385 +fun timing timing = map_transition (fn (name, pos, markers, _, trans) =>
  17.386 +  (name, pos, markers, timing, trans));
  17.387  
  17.388 -fun add_trans tr = map_transition (fn (name, pos, timing, trans) =>
  17.389 -  (name, pos, timing, tr :: trans));
  17.390 +fun add_trans tr = map_transition (fn (name, pos, markers, timing, trans) =>
  17.391 +  (name, pos, markers, timing, tr :: trans));
  17.392  
  17.393 -val reset_trans = map_transition (fn (name, pos, timing, _) =>
  17.394 -  (name, pos, timing, []));
  17.395 +val reset_trans = map_transition (fn (name, pos, markers, timing, _) =>
  17.396 +  (name, pos, markers, timing, []));
  17.397  
  17.398  
  17.399  (* basic transitions *)
  17.400 @@ -368,7 +396,7 @@
  17.401  
  17.402  fun present_transaction f g = add_trans (Transaction (f, g));
  17.403  fun transaction f = present_transaction f (K ());
  17.404 -fun transaction0 f = present_transaction (node_presentation0 oo f) (K ());
  17.405 +fun transaction0 f = present_transaction (node_presentation oo f) (K ());
  17.406  
  17.407  fun keep f = add_trans (Keep (fn _ => f));
  17.408  
  17.409 @@ -388,7 +416,7 @@
  17.410  (* theory transitions *)
  17.411  
  17.412  fun generic_theory f = transaction (fn _ =>
  17.413 -  (fn Theory gthy => node_presentation0 (Theory (f gthy))
  17.414 +  (fn Theory gthy => node_presentation (Theory (f gthy))
  17.415      | _ => raise UNDEF));
  17.416  
  17.417  fun theory' f = transaction (fn int =>
  17.418 @@ -397,7 +425,7 @@
  17.419          |> Sign.new_group
  17.420          |> f int
  17.421          |> Sign.reset_group;
  17.422 -      in node_presentation0 (Theory (Context.Theory thy')) end
  17.423 +      in node_presentation (Theory (Context.Theory thy')) end
  17.424      | _ => raise UNDEF));
  17.425  
  17.426  fun theory f = theory' (K f);
  17.427 @@ -475,15 +503,15 @@
  17.428              in (Theory gthy', ctxt') end
  17.429            else raise UNDEF
  17.430          end
  17.431 -    | Skipped_Proof (0, (gthy, _)) => node_presentation0 (Theory gthy)
  17.432 +    | Skipped_Proof (0, (gthy, _)) => node_presentation (Theory gthy)
  17.433      | _ => raise UNDEF));
  17.434  
  17.435  local
  17.436  
  17.437 -fun begin_proof init = transaction0 (fn int =>
  17.438 +fun begin_proof init_proof = transaction0 (fn int =>
  17.439    (fn Theory gthy =>
  17.440      let
  17.441 -      val (finish, prf) = init int gthy;
  17.442 +      val (finish, prf) = init_proof int gthy;
  17.443        val document = Options.default_string "document";
  17.444        val skip = (document = "" orelse document = "false") andalso Goal.skip_proofs_enabled ();
  17.445        val schematic_goal = try Proof.schematic_goal prf;
  17.446 @@ -588,9 +616,9 @@
  17.447  
  17.448  local
  17.449  
  17.450 -fun app int (tr as Transition {trans, ...}) =
  17.451 +fun app int (tr as Transition {markers, trans, ...}) =
  17.452    setmp_thread_position tr
  17.453 -    (Timing.protocol (name_of tr) (pos_of tr) (apply_trans int trans)
  17.454 +    (Timing.protocol (name_of tr) (pos_of tr) (apply_trans int trans markers)
  17.455        ##> Option.map (fn UNDEF => ERROR (type_error tr) | exn => exn));
  17.456  
  17.457  in
  17.458 @@ -690,18 +718,26 @@
  17.459          then Future.proofs_enabled 1
  17.460          else Future.proofs_enabled 2 orelse Future.proofs_enabled_timing estimate));
  17.461  
  17.462 +val empty_markers = markers [];
  17.463 +val empty_trans = reset_trans #> keep (K ());
  17.464 +
  17.465 +in
  17.466 +
  17.467 +fun fork_presentation tr = (tr |> empty_markers, tr |> empty_trans);
  17.468 +
  17.469  fun atom_result keywords tr st =
  17.470    let
  17.471      val st' =
  17.472        if Future.proofs_enabled 1 andalso Keyword.is_diag keywords (name_of tr) then
  17.473 -        (Execution.fork
  17.474 -          {name = "Toplevel.diag", pos = pos_of tr, pri = ~1}
  17.475 -          (fn () => command tr st); st)
  17.476 +        let
  17.477 +          val (tr1, tr2) = fork_presentation tr;
  17.478 +          val _ =
  17.479 +            Execution.fork {name = "Toplevel.diag", pos = pos_of tr, pri = ~1}
  17.480 +              (fn () => command tr1 st);
  17.481 +        in command tr2 st end
  17.482        else command tr st;
  17.483    in (Result (tr, st'), st') end;
  17.484  
  17.485 -in
  17.486 -
  17.487  fun element_result keywords (Thy_Element.Element (tr, NONE)) st = atom_result keywords tr st
  17.488    | element_result keywords (elem as Thy_Element.Element (head_tr, SOME element_rest)) st =
  17.489        let
  17.490 @@ -717,6 +753,8 @@
  17.491            in (Result_List (head_result :: proof_results), st'') end
  17.492          else
  17.493            let
  17.494 +            val (end_tr1, end_tr2) = fork_presentation end_tr;
  17.495 +
  17.496              val finish = Context.Theory o Proof_Context.theory_of;
  17.497  
  17.498              val future_proof =
  17.499 @@ -725,12 +763,12 @@
  17.500                    {name = "Toplevel.future_proof", pos = pos_of head_tr, pri = ~1}
  17.501                    (fn () =>
  17.502                      let
  17.503 -                      val State (SOME (Proof (prf, (_, orig_gthy)), _), prev) = st';
  17.504 +                      val State ((Proof (prf, (_, orig_gthy)), _), prev_thy) = st';
  17.505                        val node' = Proof (Proof_Node.apply (K state) prf, (finish, orig_gthy));
  17.506 -                      val (result, result_state) =
  17.507 -                        State (SOME (node_presentation0 node'), prev)
  17.508 -                        |> fold_map (element_result keywords) body_elems ||> command end_tr;
  17.509 -                    in (Result_List result, presentation_context0 result_state) end))
  17.510 +                      val (results, result_state) =
  17.511 +                        State (node_presentation node', prev_thy)
  17.512 +                        |> fold_map (element_result keywords) body_elems ||> command end_tr1;
  17.513 +                    in (Result_List results, presentation_context0 result_state) end))
  17.514                #> (fn (res, state') => state' |> put_result (Result_Future res));
  17.515  
  17.516              val forked_proof =
  17.517 @@ -739,12 +777,12 @@
  17.518                end_proof (fn _ => future_proof #>
  17.519                  (fn state => state |> Proof.global_done_proof |> Result.put (get_result state)));
  17.520  
  17.521 -            val st'' = st'
  17.522 -              |> command (head_tr |> reset_trans |> forked_proof);
  17.523 -            val end_result = Result (end_tr, st'');
  17.524 +            val st'' = st' |> command (head_tr |> reset_trans |> forked_proof);
  17.525 +            val end_st = st'' |> command end_tr2;
  17.526 +            val end_result = Result (end_tr, end_st);
  17.527              val result =
  17.528                Result_List [head_result, Result.get (presentation_context0 st''), end_result];
  17.529 -          in (result, st'') end
  17.530 +          in (result, end_st) end
  17.531        end;
  17.532  
  17.533  end;
    18.1 --- a/src/Pure/ML/ml_lex.ML	Sun Mar 10 00:22:38 2019 +0000
    18.2 +++ b/src/Pure/ML/ml_lex.ML	Sun Mar 10 21:33:05 2019 +0100
    18.3 @@ -312,7 +312,7 @@
    18.4  val scan_sml_antiq = scan_sml >> Antiquote.Text;
    18.5  
    18.6  val scan_ml_antiq =
    18.7 -  Comment.scan >> (fn (kind, ss) => Antiquote.Text (token (Comment (SOME kind)) ss)) ||
    18.8 +  Comment.scan_inner >> (fn (kind, ss) => Antiquote.Text (token (Comment (SOME kind)) ss)) ||
    18.9    Antiquote.scan_control >> Antiquote.Control ||
   18.10    Antiquote.scan_antiq >> Antiquote.Antiq ||
   18.11    scan_rat_antiq >> Antiquote.Antiq ||
    19.1 --- a/src/Pure/PIDE/command.ML	Sun Mar 10 00:22:38 2019 +0000
    19.2 +++ b/src/Pure/PIDE/command.ML	Sun Mar 10 21:33:05 2019 +0100
    19.3 @@ -155,12 +155,7 @@
    19.4          Position.here_list verbatim);
    19.5    in
    19.6      if exists #1 token_reports then Toplevel.malformed pos "Malformed command syntax"
    19.7 -    else
    19.8 -      (case Outer_Syntax.parse_tokens thy (resolve_files keywords master_dir blobs_info span) of
    19.9 -        [tr] => Toplevel.modify_init init tr
   19.10 -      | [] => Toplevel.ignored (#1 (Token.range_of span))
   19.11 -      | _ => Toplevel.malformed (#1 core_range) "Exactly one command expected")
   19.12 -      handle ERROR msg => Toplevel.malformed (#1 core_range) msg
   19.13 +    else Outer_Syntax.parse_span thy init (resolve_files keywords master_dir blobs_info span)
   19.14    end;
   19.15  
   19.16  end;
   19.17 @@ -173,7 +168,10 @@
   19.18  fun init_eval_state opt_thy =
   19.19   {failed = false,
   19.20    command = Toplevel.empty,
   19.21 -  state = (case opt_thy of NONE => Toplevel.toplevel | SOME thy => Toplevel.theory_toplevel thy)};
   19.22 +  state =
   19.23 +    (case opt_thy of
   19.24 +      NONE => Toplevel.init_toplevel ()
   19.25 +    | SOME thy => Toplevel.theory_toplevel thy)};
   19.26  
   19.27  datatype eval =
   19.28    Eval of
   19.29 @@ -214,8 +212,12 @@
   19.30  
   19.31  fun run keywords int tr st =
   19.32    if Future.proofs_enabled 1 andalso Keyword.is_diag keywords (Toplevel.name_of tr) then
   19.33 -    (Execution.fork {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1}
   19.34 -      (fn () => Toplevel.command_exception int tr st); ([], SOME st))
   19.35 +    let
   19.36 +      val (tr1, tr2) = Toplevel.fork_presentation tr;
   19.37 +      val _ =
   19.38 +        Execution.fork {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1}
   19.39 +          (fn () => Toplevel.command_exception int tr1 st);
   19.40 +    in Toplevel.command_errors int tr2 st end
   19.41    else Toplevel.command_errors int tr st;
   19.42  
   19.43  fun check_token_comments ctxt tok =
   19.44 @@ -260,10 +262,7 @@
   19.45      val errs2 =
   19.46        (case result of
   19.47          NONE => []
   19.48 -      | SOME st' =>
   19.49 -          (case try Toplevel.presentation_context st' of
   19.50 -            NONE => []
   19.51 -          | SOME ctxt' => check_span_comments ctxt' span tr));
   19.52 +      | SOME st' => check_span_comments (Toplevel.presentation_context st') span tr);
   19.53      val errs = errs1 @ errs2;
   19.54      val _ = List.app (Future.error_message (Toplevel.pos_of tr)) errs;
   19.55    in
    21.1 --- a/src/Pure/PIDE/document.ML	Sun Mar 10 00:22:38 2019 +0000
    21.2 +++ b/src/Pure/PIDE/document.ML	Sun Mar 10 21:33:05 2019 +0100
    21.3 @@ -575,7 +575,7 @@
    21.4      val imports = #imports header;
    21.5  
    21.6      fun maybe_eval_result eval = Command.eval_result_state eval
    21.7 -      handle Fail _ => Toplevel.toplevel;
    21.8 +      handle Fail _ => Toplevel.init_toplevel ();
    21.9  
   21.10      fun maybe_end_theory pos st = SOME (Toplevel.end_theory pos st)
   21.11        handle ERROR msg => (Output.error_message msg; NONE);
   21.12 @@ -586,7 +586,7 @@
   21.13            NONE =>
   21.14              maybe_end_theory pos
   21.15                (case get_result (snd (the (AList.lookup (op =) deps import))) of
   21.16 -                NONE => Toplevel.toplevel
   21.17 +                NONE => Toplevel.init_toplevel ()
   21.18                | SOME (_, eval) => maybe_eval_result eval)
   21.19          | some => some)
   21.20          |> Option.map (fn thy => (thy, (pos, Theory.get_markup thy))));
    22.1 --- a/src/Pure/PIDE/markup.ML	Sun Mar 10 00:22:38 2019 +0000
    22.2 +++ b/src/Pure/PIDE/markup.ML	Sun Mar 10 21:33:05 2019 +0100
    22.3 @@ -16,6 +16,11 @@
    22.4    val serialN: string
    22.5    val serial_properties: int -> Properties.T
    22.6    val instanceN: string
    22.7 +  val meta_titleN: string val meta_title: T
    22.8 +  val meta_creatorN: string val meta_creator: T
    22.9 +  val meta_contributorN: string val meta_contributor: T
   22.10 +  val meta_dateN: string val meta_date: T
   22.11 +  val meta_descriptionN: string val meta_description: T
   22.12    val languageN: string
   22.13    val symbolsN: string
   22.14    val delimitedN: string
   22.15 @@ -32,6 +37,7 @@
   22.16    val language_ML: bool -> T
   22.17    val language_SML: bool -> T
   22.18    val language_document: bool -> T
   22.19 +  val language_document_marker: T
   22.20    val language_antiquotation: T
   22.21    val language_text: bool -> T
   22.22    val language_verbatim: bool -> T
   22.23 @@ -282,6 +288,15 @@
   22.24  val instanceN = "instance";
   22.25  
   22.26  
   22.27 +(* meta data -- see http://dublincore.org/documents/dces *)
   22.28 +
   22.29 +val (meta_titleN, meta_title) = markup_elem "meta_title";
   22.30 +val (meta_creatorN, meta_creator) = markup_elem "meta_creator";
   22.31 +val (meta_contributorN, meta_contributor) = markup_elem "meta_contributor";
   22.32 +val (meta_dateN, meta_date) = markup_elem "meta_date";
   22.33 +val (meta_descriptionN, meta_description) = markup_elem "meta_description";
   22.34 +
   22.35 +
   22.36  (* embedded languages *)
   22.37  
   22.38  val languageN = "language";
   22.39 @@ -314,6 +329,8 @@
   22.40  val language_ML = language' {name = "ML", symbols = false, antiquotes = true};
   22.41  val language_SML = language' {name = "SML", symbols = false, antiquotes = false};
   22.42  val language_document = language' {name = "document", symbols = false, antiquotes = true};
   22.43 +val language_document_marker =
   22.44 +  language {name = "document_marker", symbols = true, antiquotes = true, delimited = true};
   22.45  val language_antiquotation =
   22.46    language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true};
   22.47  val language_text = language' {name = "text", symbols = true, antiquotes = false};
    23.1 --- a/src/Pure/PIDE/markup.scala	Sun Mar 10 00:22:38 2019 +0000
    23.2 +++ b/src/Pure/PIDE/markup.scala	Sun Mar 10 21:33:05 2019 +0100
    23.3 @@ -89,6 +89,15 @@
    23.4    }
    23.5  
    23.6  
    23.7 +  /* meta data */
    23.8 +
    23.9 +  val META_TITLE = "meta_title"
   23.10 +  val META_CREATOR = "meta_creator"
   23.11 +  val META_CONTRIBUTOR = "meta_contributor"
   23.12 +  val META_DATE = "meta_date"
   23.13 +  val META_DESCRIPTION = "meta_description"
   23.14 +
   23.15 +
   23.16    /* formal entities */
   23.17  
   23.18    val BINDING = "binding"
    25.1 --- a/src/Pure/ROOT.ML	Sun Mar 10 00:22:38 2019 +0000
    25.2 +++ b/src/Pure/ROOT.ML	Sun Mar 10 21:33:05 2019 +0100
    25.3 @@ -208,6 +208,7 @@
    25.4  ML_file "Isar/parse.ML";
    25.5  ML_file "Thy/document_source.ML";
    25.6  ML_file "Thy/thy_header.ML";
    25.7 +ML_file "Thy/document_marker.ML";
    25.8  
    25.9  (*proof context*)
   25.10  ML_file "Isar/object_logic.ML";
    26.1 --- a/src/Pure/Syntax/lexicon.ML	Sun Mar 10 00:22:38 2019 +0000
    26.2 +++ b/src/Pure/Syntax/lexicon.ML	Sun Mar 10 21:33:05 2019 +0100
    26.3 @@ -301,7 +301,7 @@
    26.4  
    26.5      val scan =
    26.6        Symbol_Pos.scan_cartouche err_prefix >> token Cartouche ||
    26.7 -      Comment.scan >> (fn (kind, ss) => token (Comment kind) ss) ||
    26.8 +      Comment.scan_inner >> (fn (kind, ss) => token (Comment kind) ss) ||
    26.9        Scan.max token_leq scan_lit scan_val ||
   26.10        scan_string >> token String ||
   26.11        scan_str >> token Str ||
    27.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    27.2 +++ b/src/Pure/Thy/document_marker.ML	Sun Mar 10 21:33:05 2019 +0100
    27.3 @@ -0,0 +1,84 @@
    27.4 +(*  Title:      Pure/Thy/document_marker.ML
    27.5 +    Author:     Makarius
    27.6 +
    27.7 +Document markers: declarations on the presentation context.
    27.8 +*)
    27.9 +
   27.10 +signature DOCUMENT_MARKER =
   27.11 +sig
   27.12 +  type marker = Proof.context -> Proof.context
   27.13 +  val setup: binding -> 'a context_parser -> ('a -> marker) -> theory -> theory
   27.14 +  val setup0: binding -> 'a parser -> ('a -> marker) -> theory -> theory
   27.15 +  val evaluate: Input.source -> marker
   27.16 +  val legacy_tag: string -> Input.source
   27.17 +end;
   27.18 +
   27.19 +structure Document_Marker: DOCUMENT_MARKER =
   27.20 +struct
   27.21 +
   27.22 +(* theory data *)
   27.23 +
   27.24 +type marker = Proof.context -> Proof.context;
   27.25 +
   27.26 +structure Markers = Theory_Data
   27.27 +(
   27.28 +  type T = (Token.src -> Proof.context -> Proof.context) Name_Space.table;
   27.29 +  val empty : T = Name_Space.empty_table "document_marker";
   27.30 +  val extend = I;
   27.31 +  val merge = Name_Space.merge_tables;
   27.32 +);
   27.33 +
   27.34 +val get_markers = Markers.get o Proof_Context.theory_of;
   27.35 +
   27.36 +fun check ctxt = Name_Space.check (Context.Proof ctxt) (get_markers ctxt);
   27.37 +
   27.38 +fun setup name scan body thy =
   27.39 +  let
   27.40 +    fun marker src ctxt =
   27.41 +      let val (x, ctxt') = Token.syntax scan src ctxt
   27.42 +      in body x ctxt' end;
   27.43 +  in thy |> Markers.map (Name_Space.define (Context.Theory thy) true (name, marker) #> #2) end;
   27.44 +
   27.45 +fun setup0 name scan = setup name (Scan.lift scan);
   27.46 +
   27.47 +
   27.48 +(* evaluate inner syntax *)
   27.49 +
   27.50 +val parse_marker = Parse.token Parse.liberal_name ::: Parse.!!! Parse.args;
   27.51 +
   27.52 +fun evaluate input ctxt =
   27.53 +  let
   27.54 +    val body =
   27.55 +      Input.source_explode input
   27.56 +      |> drop_prefix (fn (s, _) => s = Symbol.marker)
   27.57 +      |> Symbol_Pos.cartouche_content;
   27.58 +    val markers =
   27.59 +      (case Token.read_body (Thy_Header.get_keywords' ctxt) (Parse.list parse_marker) body of
   27.60 +        SOME res => res
   27.61 +      | NONE => error ("Bad input" ^ Position.here (Input.pos_of input)));
   27.62 +  in fold (fn src => #2 (check ctxt (Token.name_of_src src)) src) markers ctxt end;
   27.63 +
   27.64 +
   27.65 +(* concrete markers *)
   27.66 +
   27.67 +fun meta_data markup arg ctxt =
   27.68 +  (Context_Position.report_text ctxt (Position.thread_data ()) markup arg; ctxt);
   27.69 +
   27.70 +val _ =
   27.71 +  Theory.setup
   27.72 +    (setup0 (Binding.make ("tag", \<^here>)) Parse.name Document_Source.update_tags #>
   27.73 +     setup0 (Binding.make ("title", \<^here>)) Parse.embedded (meta_data Markup.meta_title) #>
   27.74 +     setup0 (Binding.make ("creator", \<^here>)) Parse.embedded (meta_data Markup.meta_creator) #>
   27.75 +     setup0 (Binding.make ("contributor", \<^here>)) Parse.embedded (meta_data Markup.meta_contributor) #>
   27.76 +     setup0 (Binding.make ("date", \<^here>)) Parse.embedded (meta_data Markup.meta_date) #>
   27.77 +     setup0 (Binding.make ("description", \<^here>)) (Parse.input Parse.embedded)
   27.78 +      (fn source => fn ctxt =>
   27.79 +        let
   27.80 +          val (arg, pos) = Input.source_content source;
   27.81 +          val _ = Context_Position.report ctxt pos Markup.words;
   27.82 +        in meta_data Markup.meta_description arg ctxt end));
   27.83 +
   27.84 +fun legacy_tag name =
   27.85 +  Input.string (cartouche ("tag " ^ Symbol_Pos.quote_string_qq name));
   27.86 +
   27.87 +end;
    28.1 --- a/src/Pure/Thy/document_source.ML	Sun Mar 10 00:22:38 2019 +0000
    28.2 +++ b/src/Pure/Thy/document_source.ML	Sun Mar 10 21:33:05 2019 +0100
    28.3 @@ -14,8 +14,10 @@
    28.4    val improper: Token.T list parser
    28.5    val improper_end: Token.T list parser
    28.6    val blank_end: Token.T list parser
    28.7 -  val tag: string parser
    28.8 +  val get_tags: Proof.context -> string list
    28.9 +  val update_tags: string -> Proof.context -> Proof.context
   28.10    val tags: string list parser
   28.11 +  val annotation: unit parser
   28.12  end;
   28.13  
   28.14  structure Document_Source: DOCUMENT_SOURCE =
   28.15 @@ -41,11 +43,27 @@
   28.16  val blank_end = Scan.repeat (Scan.unless space_proper (Scan.one Token.is_blank));
   28.17  
   28.18  
   28.19 -(* tags *)
   28.20 +(* syntactic tags (old-style) *)
   28.21 +
   28.22 +structure Tags = Proof_Data
   28.23 +(
   28.24 +  type T = string list;
   28.25 +  fun init _ = [];
   28.26 +);
   28.27 +
   28.28 +val get_tags = Tags.get;
   28.29 +val update_tags = Tags.map o update (op =);
   28.30  
   28.31  val tag_name = Parse.group (fn () => "document tag name") (Parse.short_ident || Parse.string);
   28.32  
   28.33  val tag = (improper -- Parse.$$$ "%" -- improper) |-- Parse.!!! (tag_name --| blank_end);
   28.34  val tags = Scan.repeat tag;
   28.35  
   28.36 +
   28.37 +(* semantic markers (operation on presentation context) *)
   28.38 +
   28.39 +val marker = improper |-- Parse.document_marker --| blank_end;
   28.40 +
   28.41 +val annotation = Scan.repeat (tag >> K () || marker >> K ()) >> K ();
   28.42 +
   28.43  end;
    29.1 --- a/src/Pure/Thy/thy_header.ML	Sun Mar 10 00:22:38 2019 +0000
    29.2 +++ b/src/Pure/Thy/thy_header.ML	Sun Mar 10 21:33:05 2019 +0100
    29.3 @@ -175,10 +175,11 @@
    29.4      Parse.command_name textN ||
    29.5      Parse.command_name txtN ||
    29.6      Parse.command_name text_rawN) --
    29.7 -  Document_Source.tags -- Parse.!!! Parse.document_source;
    29.8 +  (Document_Source.annotation |-- Parse.!!! Parse.document_source);
    29.9  
   29.10  val parse_header =
   29.11 -  (Scan.repeat heading -- Parse.command_name theoryN -- Document_Source.tags) |-- Parse.!!! args;
   29.12 +  (Scan.repeat heading -- Parse.command_name theoryN --| Document_Source.annotation)
   29.13 +    |-- Parse.!!! args;
   29.14  
   29.15  fun read_tokens pos toks =
   29.16    filter Token.is_proper toks
    30.1 --- a/src/Pure/Thy/thy_header.scala	Sun Mar 10 00:22:38 2019 +0000
    30.2 +++ b/src/Pure/Thy/thy_header.scala	Sun Mar 10 21:33:05 2019 +0100
    30.3 @@ -172,9 +172,9 @@
    30.4            command(TEXT) |
    30.5            command(TXT) |
    30.6            command(TEXT_RAW)) ~
    30.7 -        tags ~! document_source
    30.8 +        annotation ~! document_source
    30.9  
   30.10 -      (rep(heading) ~ command(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x }
   30.11 +      (rep(heading) ~ command(THEORY) ~ annotation) ~! args ^^ { case _ ~ x => x }
   30.12      }
   30.13    }
   30.14  
    31.1 --- a/src/Pure/Thy/thy_info.ML	Sun Mar 10 00:22:38 2019 +0000
    31.2 +++ b/src/Pure/Thy/thy_info.ML	Sun Mar 10 21:33:05 2019 +0100
    31.3 @@ -295,7 +295,7 @@
    31.4        in (results, (st', pos')) end;
    31.5  
    31.6      val (results, (end_state, end_pos)) =
    31.7 -      fold_map element_result elements (Toplevel.toplevel, Position.none);
    31.8 +      fold_map element_result elements (Toplevel.init_toplevel (), Position.none);
    31.9  
   31.10      val thy = Toplevel.end_theory end_pos end_state;
   31.11    in (results, thy) end;
   31.12 @@ -451,11 +451,9 @@
   31.13  
   31.14  fun script_thy pos txt thy =
   31.15    let
   31.16 -    val trs =
   31.17 -      Outer_Syntax.parse thy pos txt
   31.18 -      |> map (Toplevel.modify_init (K thy));
   31.19 +    val trs = Outer_Syntax.parse_text thy (K thy) pos txt;
   31.20      val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs);
   31.21 -    val end_state = fold (Toplevel.command_exception true) trs Toplevel.toplevel;
   31.22 +    val end_state = fold (Toplevel.command_exception true) trs (Toplevel.init_toplevel ());
   31.23    in Toplevel.end_theory end_pos end_state end;
   31.24  
   31.25  
    32.1 --- a/src/Pure/Thy/thy_output.ML	Sun Mar 10 00:22:38 2019 +0000
    32.2 +++ b/src/Pure/Thy/thy_output.ML	Sun Mar 10 21:33:05 2019 +0100
    32.3 @@ -61,8 +61,8 @@
    32.4        Symbol_Pos.cartouche_content syms
    32.5        |> output_symbols
    32.6        |> Latex.enclose_body "%\n\\isamarkupcancel{" "}"
    32.7 -  | Comment.Latex =>
    32.8 -      [Latex.symbols (Symbol_Pos.cartouche_content syms)])
    32.9 +  | Comment.Latex => [Latex.symbols (Symbol_Pos.cartouche_content syms)]
   32.10 +  | Comment.Marker => [])
   32.11  and output_comment_document ctxt (comment, syms) =
   32.12    (case comment of
   32.13      SOME kind => output_comment ctxt (kind, syms)
   32.14 @@ -139,6 +139,7 @@
   32.15    in
   32.16      (case Token.kind_of tok of
   32.17        Token.Comment NONE => []
   32.18 +    | Token.Comment (SOME Comment.Marker) => []
   32.19      | Token.Command => output false "\\isacommand{" "}"
   32.20      | Token.Keyword =>
   32.21          if Symbol.is_ascii_identifier (Token.content_of tok)
   32.22 @@ -202,7 +203,7 @@
   32.23  
   32.24  (* command spans *)
   32.25  
   32.26 -type command = string * Position.T * string list;   (*name, position, tags*)
   32.27 +type command = string * Position.T;   (*name, position*)
   32.28  type source = (token * (string * int)) list;        (*token, markup flag, meta-comment depth*)
   32.29  
   32.30  datatype span = Span of command * (source * source * source * source) * bool;
   32.31 @@ -276,18 +277,17 @@
   32.32        in {tag' = tag', active_tag' = active_tag'} end
   32.33    end;
   32.34  
   32.35 -fun present_span thy command_tag span state state'
   32.36 +fun present_span command_tag span state state'
   32.37      (tag_stack, active_tag, newline, latex, present_cont) =
   32.38    let
   32.39 -    val ctxt' =
   32.40 -      Toplevel.presentation_context state'
   32.41 -        handle Toplevel.UNDEF => Proof_Context.get_global thy Context.PureN;
   32.42 +    val ctxt' = Toplevel.presentation_context state';
   32.43      val present = fold (fn (tok, (flag, 0)) =>
   32.44          fold cons (present_token ctxt' tok)
   32.45          #> cons (Latex.string flag)
   32.46        | _ => I);
   32.47  
   32.48 -    val Span ((cmd_name, cmd_pos, cmd_tags), srcs, span_newline) = span;
   32.49 +    val Span ((cmd_name, cmd_pos), srcs, span_newline) = span;
   32.50 +    val cmd_tags = Document_Source.get_tags ctxt';
   32.51  
   32.52      val (tag, tags) = tag_stack;
   32.53      val {tag', active_tag'} =
   32.54 @@ -371,19 +371,19 @@
   32.55        Document_Source.improper |--
   32.56          Parse.position (Scan.one (fn tok =>
   32.57            Token.is_command tok andalso pred keywords (Token.content_of tok))) --
   32.58 -      Scan.repeat Document_Source.tag --
   32.59 -      Parse.!!!! ((Document_Source.improper -- locale -- Document_Source.improper) |--
   32.60 -        Parse.document_source --| Document_Source.improper_end)
   32.61 -          >> (fn (((tok, pos'), tags), source) =>
   32.62 -            let val name = Token.content_of tok
   32.63 -            in (SOME (name, pos', tags), (mk (name, source), (flag, d))) end));
   32.64 +      (Document_Source.annotation |--
   32.65 +        Parse.!!!! ((Document_Source.improper -- locale -- Document_Source.improper) |--
   32.66 +          Parse.document_source --| Document_Source.improper_end))
   32.67 +            >> (fn ((tok, pos'), source) =>
   32.68 +              let val name = Token.content_of tok
   32.69 +              in (SOME (name, pos'), (mk (name, source), (flag, d))) end));
   32.70  
   32.71      val command = Scan.peek (fn d =>
   32.72        Scan.optional (Scan.one Token.is_command_modifier ::: Document_Source.improper) [] --
   32.73 -      Scan.one Token.is_command -- Document_Source.tags
   32.74 -      >> (fn ((cmd_mod, cmd), tags) =>
   32.75 +      Scan.one Token.is_command --| Document_Source.annotation
   32.76 +      >> (fn (cmd_mod, cmd) =>
   32.77          map (fn tok => (NONE, (Basic_Token tok, ("", d)))) cmd_mod @
   32.78 -          [(SOME (Token.content_of cmd, Token.pos_of cmd, tags),
   32.79 +          [(SOME (Token.content_of cmd, Token.pos_of cmd),
   32.80              (Basic_Token cmd, (markup_false, d)))]));
   32.81  
   32.82      val cmt = Scan.peek (fn d =>
   32.83 @@ -442,14 +442,14 @@
   32.84      val command_tag = make_command_tag options keywords;
   32.85  
   32.86      fun present_command tr span st st' =
   32.87 -      Toplevel.setmp_thread_position tr (present_span thy command_tag span st st');
   32.88 +      Toplevel.setmp_thread_position tr (present_span command_tag span st st');
   32.89  
   32.90      fun present _ [] = I
   32.91        | present st ((span, (tr, st')) :: rest) = present_command tr span st st' #> present st' rest;
   32.92    in
   32.93      if length command_results = length spans then
   32.94        ((NONE, []), NONE, true, [], (I, I))
   32.95 -      |> present Toplevel.toplevel (spans ~~ command_results)
   32.96 +      |> present (Toplevel.init_toplevel ()) (spans ~~ command_results)
   32.97        |> present_trailer
   32.98        |> rev
   32.99      else error "Messed-up outer syntax for presentation"
    33.1 --- a/src/Pure/Tools/debugger.ML	Sun Mar 10 00:22:38 2019 +0000
    33.2 +++ b/src/Pure/Tools/debugger.ML	Sun Mar 10 21:33:05 2019 +0100
    33.3 @@ -279,8 +279,7 @@
    33.4              if Command.eval_finished eval then
    33.5                let
    33.6                  val st = Command.eval_result_state eval;
    33.7 -                val ctxt = Toplevel.presentation_context st
    33.8 -                  handle Toplevel.UNDEF => err ();
    33.9 +                val ctxt = Toplevel.presentation_context st;
   33.10                in
   33.11                  (case ML_Env.get_breakpoint (Context.Proof ctxt) breakpoint of
   33.12                    SOME (b, _) => b := breakpoint_state
    34.1 --- a/src/Pure/Tools/rail.ML	Sun Mar 10 00:22:38 2019 +0000
    34.2 +++ b/src/Pure/Tools/rail.ML	Sun Mar 10 21:33:05 2019 +0100
    34.3 @@ -118,7 +118,7 @@
    34.4  
    34.5  val scan_token =
    34.6    scan_space >> token Space ||
    34.7 -  Comment.scan >> (fn (kind, ss) => token (Comment kind) ss)||
    34.8 +  Comment.scan_inner >> (fn (kind, ss) => token (Comment kind) ss) ||
    34.9    Antiquote.scan_antiq >> antiq_token ||
   34.10    scan_keyword >> (token Keyword o single) ||
   34.11    Lexicon.scan_id >> token Ident ||
    35.1 --- a/src/Pure/theory.ML	Sun Mar 10 00:22:38 2019 +0000
    35.2 +++ b/src/Pure/theory.ML	Sun Mar 10 21:33:05 2019 +0100
    35.3 @@ -13,6 +13,7 @@
    35.4    val local_setup: (Proof.context -> Proof.context) -> unit
    35.5    val install_pure: theory -> unit
    35.6    val get_pure: unit -> theory
    35.7 +  val get_pure_bootstrap: unit -> theory
    35.8    val get_markup: theory -> Markup.T
    35.9    val check: {long: bool} -> Proof.context -> string * Position.T -> theory
   35.10    val axiom_table: theory -> term Name_Space.table
   35.11 @@ -59,6 +60,11 @@
   35.12      SOME thy => thy
   35.13    | NONE => raise Fail "Theory Pure not present");
   35.14  
   35.15 +fun get_pure_bootstrap () =
   35.16 +  (case Single_Assignment.peek pure of
   35.17 +    SOME thy => thy
   35.18 +  | NONE => Context.the_global_context ());
   35.19 +
   35.20  
   35.21  
   35.22  (** datatype thy **)