clarified Antiquote.antiq_reports;
authorwenzelm
Fri Oct 16 10:11:20 2015 +0200 (2015-10-16)
changeset 614573e21699bb83b
parent 61456 b521b8b400f7
child 61458 987533262fc2
clarified Antiquote.antiq_reports;
Thy_Output.output_text: support for markdown (inactive);
eliminared Thy_Output.check_text -- uniform use of Thy_Output.output_text;
src/HOL/ex/Cartouche_Examples.thy
src/Pure/General/antiquote.ML
src/Pure/ML/ml_lex.ML
src/Pure/PIDE/command.ML
src/Pure/Thy/markdown.ML
src/Pure/Thy/thy_output.ML
src/Pure/Tools/rail.ML
src/Pure/pure_syn.ML
     1.1 --- a/src/HOL/ex/Cartouche_Examples.thy	Thu Oct 15 22:25:57 2015 +0200
     1.2 +++ b/src/HOL/ex/Cartouche_Examples.thy	Fri Oct 16 10:11:20 2015 +0200
     1.3 @@ -179,7 +179,8 @@
     1.4  ML \<open>
     1.5    Outer_Syntax.command
     1.6      @{command_keyword text_cartouche} ""
     1.7 -    (Parse.opt_target -- Parse.input Parse.cartouche >> Thy_Output.document_command)
     1.8 +    (Parse.opt_target -- Parse.input Parse.cartouche
     1.9 +      >> Thy_Output.document_command {markdown = true})
    1.10  \<close>
    1.11  
    1.12  text_cartouche
     2.1 --- a/src/Pure/General/antiquote.ML	Thu Oct 15 22:25:57 2015 +0200
     2.2 +++ b/src/Pure/General/antiquote.ML	Fri Oct 16 10:11:20 2015 +0200
     2.3 @@ -11,9 +11,7 @@
     2.4    type text_antiquote = Symbol_Pos.T list antiquote
     2.5    val range: text_antiquote list -> Position.range
     2.6    val split_lines: text_antiquote list -> text_antiquote list list
     2.7 -  val antiq_reports: antiq -> Position.report list
     2.8 -  val antiquote_reports: ('a -> Position.report_text list) ->
     2.9 -    'a antiquote list -> Position.report_text list
    2.10 +  val antiq_reports: 'a antiquote list -> Position.report list
    2.11    val scan_antiq: Symbol_Pos.T list -> antiq * Symbol_Pos.T list
    2.12    val scan_antiquote: Symbol_Pos.T list -> text_antiquote * Symbol_Pos.T list
    2.13    val read': Position.T -> Symbol_Pos.T list -> text_antiquote list
    2.14 @@ -56,12 +54,13 @@
    2.15  
    2.16  (* reports *)
    2.17  
    2.18 -fun antiq_reports ((_, {start, stop, range = (pos, _)}): antiq) =
    2.19 -  [(start, Markup.antiquote), (stop, Markup.antiquote),
    2.20 -   (pos, Markup.antiquoted), (pos, Markup.language_antiquotation)];
    2.21 -
    2.22 -fun antiquote_reports text =
    2.23 -  maps (fn Text x => text x | Antiq antiq => map (rpair "") (antiq_reports antiq));
    2.24 +fun antiq_reports ants = ants |> maps
    2.25 +  (fn Antiq (_, {start, stop, range = (pos, _)}) =>
    2.26 +      [(start, Markup.antiquote),
    2.27 +       (stop, Markup.antiquote),
    2.28 +       (pos, Markup.antiquoted),
    2.29 +       (pos, Markup.language_antiquotation)]
    2.30 +    | _ => []);
    2.31  
    2.32  
    2.33  (* scan *)
    2.34 @@ -102,7 +101,7 @@
    2.35  
    2.36  fun read' pos syms =
    2.37    (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote) syms of
    2.38 -    SOME xs => (Position.reports_text (antiquote_reports (K []) xs); xs)
    2.39 +    SOME ants => (Position.reports (antiq_reports ants); ants)
    2.40    | NONE => error ("Malformed quotation/antiquotation source" ^ Position.here pos));
    2.41  
    2.42  fun read source = read' (Input.pos_of source) (Input.source_explode source);
     3.1 --- a/src/Pure/ML/ml_lex.ML	Thu Oct 15 22:25:57 2015 +0200
     3.2 +++ b/src/Pure/ML/ml_lex.ML	Fri Oct 16 10:11:20 2015 +0200
     3.3 @@ -157,7 +157,7 @@
     3.4  
     3.5  in
     3.6  
     3.7 -fun report_of_token SML (tok as Token ((pos, _), (kind, x))) =
     3.8 +fun token_report SML (tok as Token ((pos, _), (kind, x))) =
     3.9    let
    3.10      val (markup, txt) =
    3.11        if not (is_keyword tok) then token_kind_markup SML kind
    3.12 @@ -328,7 +328,8 @@
    3.13          (Scan.recover (Scan.bulk (!!! "bad input" scan))
    3.14            (fn msg => recover msg >> map Antiquote.Text))
    3.15        |> Source.exhaust
    3.16 -      |> tap (Position.reports_text o Antiquote.antiquote_reports (single o report_of_token SML))
    3.17 +      |> tap (Position.reports o Antiquote.antiq_reports)
    3.18 +      |> tap (Position.reports_text o maps (fn Antiquote.Text t => [token_report SML t] | _ => []))
    3.19        |> tap (List.app check);
    3.20    in input @ termination end;
    3.21  
     4.1 --- a/src/Pure/PIDE/command.ML	Thu Oct 15 22:25:57 2015 +0200
     4.2 +++ b/src/Pure/PIDE/command.ML	Fri Oct 16 10:11:20 2015 +0200
     4.3 @@ -193,7 +193,7 @@
     4.4    Toplevel.setmp_thread_position tr
     4.5      (fn () =>
     4.6        Outer_Syntax.side_comments span |> maps (fn cmt =>
     4.7 -        (Thy_Output.check_text (Token.input_of cmt) st'; [])
     4.8 +        (Thy_Output.output_text st' {markdown = false} (Token.input_of cmt); [])
     4.9            handle exn =>
    4.10              if Exn.is_interrupt exn then reraise exn
    4.11              else Runtime.exn_messages_ids exn)) ();
     5.1 --- a/src/Pure/Thy/markdown.ML	Thu Oct 15 22:25:57 2015 +0200
     5.2 +++ b/src/Pure/Thy/markdown.ML	Fri Oct 16 10:11:20 2015 +0200
     5.3 @@ -19,6 +19,7 @@
     5.4  
     5.5  signature MARKDOWN =
     5.6  sig
     5.7 +  val is_control: Symbol.symbol -> bool
     5.8    datatype kind = Itemize | Enumerate | Description
     5.9    val print_kind: kind -> string
    5.10    type marker = {indent: int, kind: kind}
    5.11 @@ -29,7 +30,9 @@
    5.12    val empty_line: line
    5.13    datatype block = Paragraph of line list | List of marker * block list
    5.14    val read_lines: line list -> block list
    5.15 -  val read: Input.source -> block list
    5.16 +  val read_antiquotes: Antiquote.text_antiquote list -> block list
    5.17 +  val read_source: Input.source -> block list
    5.18 +  val text_reports: Antiquote.text_antiquote list -> Position.report list
    5.19    val reports: block list -> Position.report list
    5.20  end;
    5.21  
    5.22 @@ -38,6 +41,8 @@
    5.23  
    5.24  (* document lines *)
    5.25  
    5.26 +val is_control = member (op =) ["\\<^item>", "\\<^enum>", "\\<^descr>"];
    5.27 +
    5.28  datatype kind = Itemize | Enumerate | Description;
    5.29  
    5.30  fun print_kind Itemize = "itemize"
    5.31 @@ -155,17 +160,22 @@
    5.32      (Scan.repeat (Scan.many line_is_empty |-- parse_document) --| Scan.many line_is_empty) #>
    5.33    the_default [] #> flat;
    5.34  
    5.35 -end;
    5.36 +val read_antiquotes = Antiquote.split_lines #> map make_line #> read_lines;
    5.37 +val read_source = Antiquote.read #> read_antiquotes;
    5.38  
    5.39 -val read = Antiquote.read #> Antiquote.split_lines #> map make_line #> read_lines;
    5.40 +end;
    5.41  
    5.42  
    5.43  (* PIDE reports *)
    5.44  
    5.45 +val text_reports =
    5.46 +  maps (fn Antiquote.Text ss => [(#1 (Symbol_Pos.range ss), Markup.words)] | _ => []);
    5.47 +
    5.48  local
    5.49  
    5.50 -fun line_reports depth (Line {marker = SOME (_, pos), ...}) =
    5.51 -      cons (pos, Markup.markdown_item depth)
    5.52 +fun line_reports depth (Line {marker = SOME (_, pos), content, ...}) =
    5.53 +      cons (pos, Markup.markdown_item depth) #>
    5.54 +      append (text_reports content)
    5.55    | line_reports _ _ = I;
    5.56  
    5.57  fun block_reports depth block =
     6.1 --- a/src/Pure/Thy/thy_output.ML	Thu Oct 15 22:25:57 2015 +0200
     6.2 +++ b/src/Pure/Thy/thy_output.ML	Fri Oct 16 10:11:20 2015 +0200
     6.3 @@ -24,8 +24,7 @@
     6.4    val boolean: string -> bool
     6.5    val integer: string -> int
     6.6    val eval_antiquote: Toplevel.state -> Antiquote.text_antiquote -> string
     6.7 -  val report_text: Input.source -> unit
     6.8 -  val check_text: Input.source -> Toplevel.state -> unit
     6.9 +  val output_text: Toplevel.state -> {markdown: bool} -> Input.source -> string
    6.10    val present_thy: theory -> (Toplevel.transition * Toplevel.state) list -> Token.T list -> Buffer.T
    6.11    val pretty_text: Proof.context -> string -> Pretty.T
    6.12    val pretty_term: Proof.context -> term -> Pretty.T
    6.13 @@ -37,7 +36,7 @@
    6.14    val output: Proof.context -> Pretty.T list -> string
    6.15    val verbatim_text: Proof.context -> string -> string
    6.16    val old_header_command: Input.source -> Toplevel.transition -> Toplevel.transition
    6.17 -  val document_command: (xstring * Position.T) option * Input.source ->
    6.18 +  val document_command: {markdown: bool} -> (xstring * Position.T) option * Input.source ->
    6.19      Toplevel.transition -> Toplevel.transition
    6.20  end;
    6.21  
    6.22 @@ -160,17 +159,7 @@
    6.23  end;
    6.24  
    6.25  
    6.26 -(* eval antiquotes *)
    6.27 -
    6.28 -fun read_antiquotes state source =
    6.29 -  let
    6.30 -    val ants =
    6.31 -      Antiquote.read' (Input.pos_of source) (Symbol_Pos.trim_blanks (Input.source_explode source));
    6.32 -
    6.33 -    fun words (Antiquote.Text ss) = [(#1 (Symbol_Pos.range ss), Markup.words)]
    6.34 -      | words (Antiquote.Antiq _) = [];
    6.35 -    val _ = Position.reports (maps words ants);
    6.36 -  in ants end;
    6.37 +(* eval antiquote *)
    6.38  
    6.39  fun eval_antiquote _ (Antiquote.Text ss) = Symbol_Pos.content ss
    6.40    | eval_antiquote state (Antiquote.Antiq (ss, {range = (pos, _), ...})) =
    6.41 @@ -192,18 +181,42 @@
    6.42        in Print_Mode.with_modes print_modes (fn () => cmd print_ctxt) () end;
    6.43  
    6.44  
    6.45 -(* check_text *)
    6.46 +(* output text *)
    6.47  
    6.48 -fun report_text source =
    6.49 -  Position.report (Input.pos_of source) (Markup.language_document (Input.is_delimited source));
    6.50 +fun output_text state {markdown} source =
    6.51 +  let
    6.52 +    val pos = Input.pos_of source;
    6.53 +    val _ = Position.report pos (Markup.language_document (Input.is_delimited source));
    6.54 +    val syms = Input.source_explode source;
    6.55 +
    6.56 +    val output_antiquote = eval_antiquote state #> Symbol.explode #> Latex.output_ctrl_symbols;
    6.57 +    val output_antiquotes = map output_antiquote #> implode;
    6.58  
    6.59 -fun check_text source state =
    6.60 - (report_text source;
    6.61 -  if Toplevel.is_skipped_proof state then ()
    6.62 -  else
    6.63 -    source
    6.64 -    |> read_antiquotes state
    6.65 -    |> List.app (ignore o eval_antiquote state));
    6.66 +    fun output_blocks blocks = space_implode "\n\n" (map output_block blocks)
    6.67 +    and output_block (Markdown.Paragraph lines) =
    6.68 +          cat_lines (map (output_antiquotes o Markdown.line_source) lines)
    6.69 +      | output_block (Markdown.List (marker, body)) =
    6.70 +          let val env = Markdown.print_kind (#kind marker) in
    6.71 +            "%\n\\begin{" ^ env ^ "}%\n" ^
    6.72 +            output_blocks body ^
    6.73 +            "%\n\\end{" ^ env ^ "}%\n"
    6.74 +          end;
    6.75 +  in
    6.76 +    if Toplevel.is_skipped_proof state then ""
    6.77 +    else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms
    6.78 +      andalso false (* FIXME *)
    6.79 +    then
    6.80 +      let
    6.81 +        val ants = Antiquote.read' pos syms;
    6.82 +        val blocks = Markdown.read_antiquotes ants;
    6.83 +        val _ = Position.reports (Markdown.reports blocks);
    6.84 +      in output_blocks blocks end
    6.85 +    else
    6.86 +      let
    6.87 +        val ants = Antiquote.read' pos (Symbol_Pos.trim_blanks syms);
    6.88 +        val _ = Position.reports (Markdown.text_reports ants);
    6.89 +      in output_antiquotes ants end
    6.90 +  end;
    6.91  
    6.92  
    6.93  
    6.94 @@ -232,21 +245,18 @@
    6.95  
    6.96  (* output token *)
    6.97  
    6.98 -fun output_token state =
    6.99 -  let
   6.100 -    val make_text = read_antiquotes state #> map (eval_antiquote state) #> implode;
   6.101 -    val output_text = make_text #> Symbol.explode #> Latex.output_ctrl_symbols;
   6.102 -    fun output No_Token = ""
   6.103 -      | output (Basic_Token tok) = Latex.output_token tok
   6.104 -      | output (Markup_Token (cmd, source)) =
   6.105 -          "%\n\\isamarkup" ^ cmd ^ "{" ^ output_text source ^ "%\n}\n"
   6.106 -      | output (Markup_Env_Token (cmd, source)) =
   6.107 -          "%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^
   6.108 -          output_text source ^
   6.109 -          "%\n\\end{isamarkup" ^ cmd ^ "}%\n"
   6.110 -      | output (Raw_Token source) =
   6.111 -          "%\n" ^ output_text source ^ "\n";
   6.112 -  in output end;
   6.113 +fun output_token state tok =
   6.114 +  (case tok of
   6.115 +    No_Token => ""
   6.116 +  | Basic_Token tok => Latex.output_token tok
   6.117 +  | Markup_Token (cmd, source) =>
   6.118 +      "%\n\\isamarkup" ^ cmd ^ "{" ^ output_text state {markdown = false} source ^ "%\n}\n"
   6.119 +  | Markup_Env_Token (cmd, source) =>
   6.120 +      "%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^
   6.121 +      output_text state {markdown = true} source ^
   6.122 +      "%\n\\end{isamarkup" ^ cmd ^ "}%\n"
   6.123 +  | Raw_Token source =>
   6.124 +      "%\n" ^ output_text state {markdown = true} source ^ "\n");
   6.125  
   6.126  
   6.127  (* command spans *)
   6.128 @@ -729,15 +739,15 @@
   6.129    Toplevel.keep (fn state =>
   6.130      if Toplevel.is_toplevel state then
   6.131       (legacy_feature "Obsolete 'header' command -- use 'chapter', 'section' etc. instead";
   6.132 -      check_text txt state)
   6.133 +      ignore (output_text state {markdown = false} txt))
   6.134      else raise Toplevel.UNDEF);
   6.135  
   6.136 -fun document_command (loc, txt) =
   6.137 +fun document_command markdown (loc, txt) =
   6.138    Toplevel.keep (fn state =>
   6.139      (case loc of
   6.140 -      NONE => check_text txt state
   6.141 +      NONE => ignore (output_text state markdown txt)
   6.142      | SOME (_, pos) =>
   6.143          error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
   6.144 -  Toplevel.present_local_theory loc (check_text txt);
   6.145 +  Toplevel.present_local_theory loc (fn state => ignore (output_text state markdown txt));
   6.146  
   6.147  end;
     7.1 --- a/src/Pure/Tools/rail.ML	Thu Oct 15 22:25:57 2015 +0200
     7.2 +++ b/src/Pure/Tools/rail.ML	Fri Oct 16 10:11:20 2015 +0200
     7.3 @@ -63,7 +63,7 @@
     7.4  fun reports_of_token (Token ((pos, _), (String, _))) = [(pos, Markup.inner_string)]
     7.5    | reports_of_token (Token ((pos, _), (Keyword, x))) =
     7.6        map (pair pos) (the_list (Symtab.lookup keywords x) @ Completion.suppress_abbrevs x)
     7.7 -  | reports_of_token (Token (_, (Antiq antiq, _))) = Antiquote.antiq_reports antiq
     7.8 +  | reports_of_token (Token (_, (Antiq antiq, _))) = Antiquote.antiq_reports [Antiquote.Antiq antiq]
     7.9    | reports_of_token _ = [];
    7.10  
    7.11  
     8.1 --- a/src/Pure/pure_syn.ML	Thu Oct 15 22:25:57 2015 +0200
     8.2 +++ b/src/Pure/pure_syn.ML	Fri Oct 16 10:11:20 2015 +0200
     8.3 @@ -19,31 +19,31 @@
     8.4  
     8.5  val _ =
     8.6    Outer_Syntax.command ("chapter", @{here}) "chapter heading"
     8.7 -    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
     8.8 +    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false});
     8.9  
    8.10  val _ =
    8.11    Outer_Syntax.command ("section", @{here}) "section heading"
    8.12 -    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
    8.13 +    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false});
    8.14  
    8.15  val _ =
    8.16    Outer_Syntax.command ("subsection", @{here}) "subsection heading"
    8.17 -    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
    8.18 +    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false});
    8.19  
    8.20  val _ =
    8.21    Outer_Syntax.command ("subsubsection", @{here}) "subsubsection heading"
    8.22 -    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
    8.23 +    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false});
    8.24  
    8.25  val _ =
    8.26    Outer_Syntax.command ("text", @{here}) "formal comment (primary style)"
    8.27 -    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
    8.28 +    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});
    8.29  
    8.30  val _ =
    8.31    Outer_Syntax.command ("txt", @{here}) "formal comment (secondary style)"
    8.32 -    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
    8.33 +    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});
    8.34  
    8.35  val _ =
    8.36    Outer_Syntax.command ("text_raw", @{here}) "raw LaTeX text"
    8.37 -    (Parse.document_source >> (fn s => Toplevel.keep (fn _ => Thy_Output.report_text s)));
    8.38 +    (Parse.document_source >> (fn s => Thy_Output.document_command {markdown = true} (NONE, s)));
    8.39  
    8.40  val _ =
    8.41    Outer_Syntax.command ("theory", @{here}) "begin theory"