more uniform treatment of formal comments within document source;
authorwenzelm
Sat Feb 03 20:34:26 2018 +0100 (16 months ago)
changeset 67571f858fe5531ac
parent 67570 c1fe89e9a00b
child 67572 a93cf1d6ba87
more uniform treatment of formal comments within document source;
more robust nesting;
lib/texinputs/isabelle.sty
src/Pure/General/antiquote.ML
src/Pure/General/comment.ML
src/Pure/Thy/document_antiquotation.ML
src/Pure/Thy/markdown.ML
src/Pure/Thy/thy_output.ML
src/Pure/Tools/rail.ML
     1.1 --- a/lib/texinputs/isabelle.sty	Sat Feb 03 15:34:22 2018 +0100
     1.2 +++ b/lib/texinputs/isabelle.sty	Sat Feb 03 20:34:26 2018 +0100
     1.3 @@ -239,7 +239,7 @@
     1.4  % cancel text
     1.5  
     1.6  \usepackage[normalem]{ulem}
     1.7 -\newcommand{\isamarkupcancel}[1]{\xout{#1}}
     1.8 +\newcommand{\isamarkupcancel}[1]{\isa{\xout{#1}}}
     1.9  
    1.10  
    1.11  % tagged regions
     2.1 --- a/src/Pure/General/antiquote.ML	Sat Feb 03 15:34:22 2018 +0100
     2.2 +++ b/src/Pure/General/antiquote.ML	Sat Feb 03 20:34:26 2018 +0100
     2.3 @@ -17,8 +17,9 @@
     2.4    val scan_control: control scanner
     2.5    val scan_antiq: antiq scanner
     2.6    val scan_antiquote: text_antiquote scanner
     2.7 -  val parse: Position.T -> Symbol_Pos.T list -> text_antiquote list
     2.8 -  val read: Input.source -> text_antiquote list
     2.9 +  val scan_antiquote_comments: text_antiquote scanner
    2.10 +  val parse_comments: Position.T -> Symbol_Pos.T list -> text_antiquote list
    2.11 +  val read_comments: Input.source -> text_antiquote list
    2.12  end;
    2.13  
    2.14  structure Antiquote: ANTIQUOTE =
    2.15 @@ -79,14 +80,24 @@
    2.16  val err_prefix = "Antiquotation lexical error: ";
    2.17  
    2.18  val scan_nl = Scan.one (fn (s, _) => s = "\n") >> single;
    2.19 +val scan_nl_opt = Scan.optional scan_nl [];
    2.20  
    2.21 -val scan_txt =
    2.22 -  scan_nl ||
    2.23 -  Scan.repeats1
    2.24 -   (Scan.many1 (fn (s, _) =>
    2.25 -      not (Symbol.is_control s) andalso s <> Symbol.open_ andalso s <> "@" andalso
    2.26 -        s <> "\n" andalso Symbol.not_eof s) ||
    2.27 -    $$$ "@" --| Scan.ahead (~$$ "{")) @@@ Scan.optional scan_nl [];
    2.28 +val scan_plain_txt =
    2.29 +  Scan.many1 (fn (s, _) =>
    2.30 +    not (Comment.is_symbol s) andalso
    2.31 +    not (Symbol.is_control s) andalso
    2.32 +    s <> Symbol.open_ andalso
    2.33 +    s <> "@" andalso
    2.34 +    s <> "\n" andalso
    2.35 +    Symbol.not_eof s) ||
    2.36 +  Scan.one (Comment.is_symbol o Symbol_Pos.symbol) >> single ||
    2.37 +  $$$ "@" --| Scan.ahead (~$$ "{");
    2.38 +
    2.39 +val scan_text =
    2.40 +  scan_nl || Scan.repeats1 scan_plain_txt @@@ scan_nl_opt;
    2.41 +
    2.42 +val scan_text_comments =
    2.43 +  scan_nl || Scan.repeats1 (Comment.scan >> #2 || scan_plain_txt) @@@ scan_nl_opt;
    2.44  
    2.45  val scan_antiq_body =
    2.46    Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 ||
    2.47 @@ -122,21 +133,24 @@
    2.48         body = body});
    2.49  
    2.50  val scan_antiquote =
    2.51 -  scan_txt >> Text || scan_control >> Control || scan_antiq >> Antiq;
    2.52 +  scan_text >> Text || scan_control >> Control || scan_antiq >> Antiq;
    2.53 +
    2.54 +val scan_antiquote_comments =
    2.55 +  scan_text_comments >> Text || scan_control >> Control || scan_antiq >> Antiq;
    2.56  
    2.57  end;
    2.58  
    2.59  
    2.60 -(* read *)
    2.61 +(* parse and read (with formal comments) *)
    2.62  
    2.63 -fun parse pos syms =
    2.64 -  (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote) syms of
    2.65 +fun parse_comments pos syms =
    2.66 +  (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote_comments) syms of
    2.67      SOME ants => ants
    2.68    | NONE => error ("Malformed quotation/antiquotation source" ^ Position.here pos));
    2.69  
    2.70 -fun read source =
    2.71 +fun read_comments source =
    2.72    let
    2.73 -    val ants = parse (Input.pos_of source) (Input.source_explode source);
    2.74 +    val ants = parse_comments (Input.pos_of source) (Input.source_explode source);
    2.75      val _ = Position.reports (antiq_reports ants);
    2.76    in ants end;
    2.77  
     3.1 --- a/src/Pure/General/comment.ML	Sat Feb 03 15:34:22 2018 +0100
     3.2 +++ b/src/Pure/General/comment.ML	Sat Feb 03 20:34:26 2018 +0100
     3.3 @@ -8,6 +8,7 @@
     3.4  sig
     3.5    datatype kind = Comment | Cancel | Latex
     3.6    val markups: kind -> Markup.T list
     3.7 +  val is_symbol: Symbol.symbol -> bool
     3.8    val scan_comment: (kind * Symbol_Pos.T list) scanner
     3.9    val scan_cancel: (kind * Symbol_Pos.T list) scanner
    3.10    val scan_latex: (kind * Symbol_Pos.T list) scanner
     4.1 --- a/src/Pure/Thy/document_antiquotation.ML	Sat Feb 03 15:34:22 2018 +0100
     4.2 +++ b/src/Pure/Thy/document_antiquotation.ML	Sat Feb 03 20:34:26 2018 +0100
     4.3 @@ -29,7 +29,8 @@
     4.4    val setup_option: binding -> (string -> Proof.context -> Proof.context) -> theory -> theory
     4.5    val boolean: string -> bool
     4.6    val integer: string -> int
     4.7 -  val evaluate: Proof.context -> Antiquote.text_antiquote -> Latex.text list
     4.8 +  val evaluate: (Symbol_Pos.T list -> Latex.text list) -> Proof.context ->
     4.9 +    Antiquote.text_antiquote -> Latex.text list
    4.10  end;
    4.11  
    4.12  structure Document_Antiquotation: DOCUMENT_ANTIQUOTATION =
    4.13 @@ -167,9 +168,9 @@
    4.14  
    4.15  in
    4.16  
    4.17 -fun evaluate ctxt antiq =
    4.18 +fun evaluate eval_text ctxt antiq =
    4.19    (case antiq of
    4.20 -    Antiquote.Text ss => [Latex.symbols ss]
    4.21 +    Antiquote.Text ss => eval_text ss
    4.22    | Antiquote.Control {name, body, ...} =>
    4.23        eval ctxt ([], Token.make_src name (if null body then [] else [Token.read_cartouche body]))
    4.24    | Antiquote.Antiq {range = (pos, _), body, ...} =>
     5.1 --- a/src/Pure/Thy/markdown.ML	Sat Feb 03 15:34:22 2018 +0100
     5.2 +++ b/src/Pure/Thy/markdown.ML	Sat Feb 03 20:34:26 2018 +0100
     5.3 @@ -191,7 +191,7 @@
     5.4    the_default [] #> flat;
     5.5  
     5.6  val read_antiquotes = Antiquote.split_lines #> map make_line #> read_lines;
     5.7 -val read_source = Antiquote.read #> read_antiquotes;
     5.8 +val read_source = Antiquote.read_comments #> read_antiquotes;
     5.9  
    5.10  end;
    5.11  
     6.1 --- a/src/Pure/Thy/thy_output.ML	Sat Feb 03 15:34:22 2018 +0100
     6.2 +++ b/src/Pure/Thy/thy_output.ML	Sat Feb 03 20:34:26 2018 +0100
     6.3 @@ -40,12 +40,36 @@
     6.4  
     6.5  (* output document source *)
     6.6  
     6.7 -fun output_document ctxt {markdown} source =
     6.8 +val output_symbols = single o Latex.symbols_output;
     6.9 +
    6.10 +fun output_comment ctxt (kind, syms) =
    6.11 +  (case kind of
    6.12 +    Comment.Comment =>
    6.13 +      Input.cartouche_content syms
    6.14 +      |> output_document (ctxt |> Config.put Document_Antiquotation.thy_output_display false)
    6.15 +          {markdown = false}
    6.16 +      |> Latex.enclose_body "%\n\\isamarkupcmt{" "%\n}"
    6.17 +  | Comment.Cancel =>
    6.18 +      Symbol_Pos.cartouche_content syms
    6.19 +      |> output_symbols
    6.20 +      |> Latex.enclose_body "%\n\\isamarkupcancel{" "}"
    6.21 +  | Comment.Latex =>
    6.22 +      [Latex.symbols (Symbol_Pos.cartouche_content syms)])
    6.23 +and output_comment_document ctxt (comment, syms) =
    6.24 +  (case comment of
    6.25 +    SOME kind => output_comment ctxt (kind, syms)
    6.26 +  | NONE => [Latex.symbols syms])
    6.27 +and output_document_text ctxt syms =
    6.28 +  (case Comment.read_body syms of
    6.29 +    SOME res => maps (output_comment_document ctxt) res
    6.30 +  | NONE => [Latex.symbols syms])
    6.31 +and output_document ctxt {markdown} source =
    6.32    let
    6.33      val pos = Input.pos_of source;
    6.34      val syms = Input.source_explode source;
    6.35  
    6.36 -    val output_antiquotes = maps (Document_Antiquotation.evaluate ctxt);
    6.37 +    val output_antiquotes =
    6.38 +      maps (Document_Antiquotation.evaluate (output_document_text ctxt) ctxt);
    6.39  
    6.40      fun output_line line =
    6.41        (if Markdown.line_is_item line then [Latex.string "\\item "] else []) @
    6.42 @@ -61,14 +85,14 @@
    6.43      else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms
    6.44      then
    6.45        let
    6.46 -        val ants = Antiquote.parse pos syms;
    6.47 +        val ants = Antiquote.parse_comments pos syms;
    6.48          val reports = Antiquote.antiq_reports ants;
    6.49          val blocks = Markdown.read_antiquotes ants;
    6.50          val _ = Context_Position.reports ctxt (reports @ Markdown.reports blocks);
    6.51        in output_blocks blocks end
    6.52      else
    6.53        let
    6.54 -        val ants = Antiquote.parse pos (trim (Symbol.is_blank o Symbol_Pos.symbol) syms);
    6.55 +        val ants = Antiquote.parse_comments pos (trim (Symbol.is_blank o Symbol_Pos.symbol) syms);
    6.56          val reports = Antiquote.antiq_reports ants;
    6.57          val _ = Context_Position.reports ctxt (reports @ Markdown.text_reports ants);
    6.58        in output_antiquotes ants end
    6.59 @@ -79,8 +103,6 @@
    6.60  
    6.61  local
    6.62  
    6.63 -val output_symbols = single o Latex.symbols_output;
    6.64 -
    6.65  val output_symbols_antiq =
    6.66    (fn Antiquote.Text syms => output_symbols syms
    6.67      | Antiquote.Control {name = (name, _), body, ...} =>
    6.68 @@ -89,32 +111,19 @@
    6.69      | Antiquote.Antiq {body, ...} =>
    6.70          Latex.enclose_body "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n" (output_symbols body));
    6.71  
    6.72 -fun output_symbols_comment ctxt {antiq} (comment, syms) =
    6.73 +fun output_comment_symbols ctxt {antiq} (comment, syms) =
    6.74    (case (comment, antiq) of
    6.75      (NONE, false) => output_symbols syms
    6.76    | (NONE, true) =>
    6.77 -      Antiquote.parse (#1 (Symbol_Pos.range syms)) syms
    6.78 +      Antiquote.parse_comments (#1 (Symbol_Pos.range syms)) syms
    6.79        |> maps output_symbols_antiq
    6.80 -  | (SOME Comment.Comment, _) =>
    6.81 -      let
    6.82 -        val source = Input.cartouche_content syms;
    6.83 -        val ctxt' = ctxt
    6.84 -          |> Config.put Document_Antiquotation.thy_output_display false;
    6.85 -      in
    6.86 -        output_document ctxt' {markdown = false} source
    6.87 -        |> Latex.enclose_body "%\n\\isamarkupcmt{" "%\n}"
    6.88 -      end
    6.89 -  | (SOME Comment.Cancel, _) =>
    6.90 -      output_symbols (Symbol_Pos.cartouche_content syms)
    6.91 -      |> Latex.enclose_body "%\n\\isamarkupcancel{" "}"
    6.92 -  | (SOME Comment.Latex, _) =>
    6.93 -      [Latex.symbols (Symbol_Pos.cartouche_content syms)]);
    6.94 +  | (SOME comment, _) => output_comment ctxt (comment, syms));
    6.95  
    6.96  in
    6.97  
    6.98  fun output_body ctxt antiq bg en syms =
    6.99    (case Comment.read_body syms of
   6.100 -    SOME res => maps (output_symbols_comment ctxt {antiq = antiq}) res
   6.101 +    SOME res => maps (output_comment_symbols ctxt {antiq = antiq}) res
   6.102    | NONE => output_symbols syms) |> Latex.enclose_body bg en
   6.103  and output_token ctxt tok =
   6.104    let
   6.105 @@ -145,7 +154,7 @@
   6.106        val _ =
   6.107          comment |> Option.app (fn kind =>
   6.108            Context_Position.reports ctxt (map (pair pos) (Markup.cartouche :: Comment.markups kind)));
   6.109 -      val _ = output_symbols_comment ctxt {antiq = false} (comment, syms);
   6.110 +      val _ = output_comment_symbols ctxt {antiq = false} (comment, syms);
   6.111      in if comment = SOME Comment.Comment then check_comments ctxt syms else () end);
   6.112  
   6.113  end;
     7.1 --- a/src/Pure/Tools/rail.ML	Sat Feb 03 15:34:22 2018 +0100
     7.2 +++ b/src/Pure/Tools/rail.ML	Sat Feb 03 20:34:26 2018 +0100
     7.3 @@ -340,7 +340,9 @@
     7.4  fun output_rules ctxt rules =
     7.5    let
     7.6      val output_antiq =
     7.7 -      Latex.output_text o Document_Antiquotation.evaluate ctxt o Antiquote.Antiq;
     7.8 +      Antiquote.Antiq #>
     7.9 +      Document_Antiquotation.evaluate (single o Latex.symbols) ctxt #>
    7.10 +      Latex.output_text;
    7.11      fun output_text b s =
    7.12        Output.output s
    7.13        |> b ? enclose "\\isakeyword{" "}"