trim_blanks after read, before eval;
authorwenzelm
Thu Oct 15 22:25:57 2015 +0200 (2015-10-15)
changeset 61456b521b8b400f7
parent 61455 0e4c257358cf
child 61457 3e21699bb83b
trim_blanks after read, before eval;
clarified Raw_Token: uniform output_text;
tuned signature;
src/Pure/General/antiquote.ML
src/Pure/General/symbol_pos.ML
src/Pure/Thy/thy_output.ML
src/Pure/Tools/rail.ML
     1.1 --- a/src/Pure/General/antiquote.ML	Thu Oct 15 21:17:41 2015 +0200
     1.2 +++ b/src/Pure/General/antiquote.ML	Thu Oct 15 22:25:57 2015 +0200
     1.3 @@ -16,6 +16,7 @@
     1.4      'a antiquote list -> Position.report_text list
     1.5    val scan_antiq: Symbol_Pos.T list -> antiq * Symbol_Pos.T list
     1.6    val scan_antiquote: Symbol_Pos.T list -> text_antiquote * Symbol_Pos.T list
     1.7 +  val read': Position.T -> Symbol_Pos.T list -> text_antiquote list
     1.8    val read: Input.source -> text_antiquote list
     1.9  end;
    1.10  
    1.11 @@ -99,10 +100,11 @@
    1.12  
    1.13  (* read *)
    1.14  
    1.15 -fun read source =
    1.16 -  (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote) (Input.source_explode source) of
    1.17 +fun read' pos syms =
    1.18 +  (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote) syms of
    1.19      SOME xs => (Position.reports_text (antiquote_reports (K []) xs); xs)
    1.20 -  | NONE =>
    1.21 -      error ("Malformed quotation/antiquotation source" ^ Position.here (Input.pos_of source)));
    1.22 +  | NONE => error ("Malformed quotation/antiquotation source" ^ Position.here pos));
    1.23 +
    1.24 +fun read source = read' (Input.pos_of source) (Input.source_explode source);
    1.25  
    1.26  end;
     2.1 --- a/src/Pure/General/symbol_pos.ML	Thu Oct 15 21:17:41 2015 +0200
     2.2 +++ b/src/Pure/General/symbol_pos.ML	Thu Oct 15 22:25:57 2015 +0200
     2.3 @@ -14,6 +14,7 @@
     2.4    val ~$$$ : Symbol.symbol -> T list -> T list * T list
     2.5    val content: T list -> string
     2.6    val range: T list -> Position.range
     2.7 +  val trim_blanks: T list -> T list
     2.8    val is_eof: T -> bool
     2.9    val stopper: T Scan.stopper
    2.10    val !!! : Scan.message -> (T list -> 'a) -> T list -> 'a
    2.11 @@ -59,6 +60,10 @@
    2.12        in Position.range pos pos' end
    2.13    | range [] = Position.no_range;
    2.14  
    2.15 +val trim_blanks =
    2.16 +  take_prefix (Symbol.is_blank o symbol) #> #2 #>
    2.17 +  take_suffix (Symbol.is_blank o symbol) #> #1;
    2.18 +
    2.19  
    2.20  (* stopper *)
    2.21  
     3.1 --- a/src/Pure/Thy/thy_output.ML	Thu Oct 15 21:17:41 2015 +0200
     3.2 +++ b/src/Pure/Thy/thy_output.ML	Thu Oct 15 22:25:57 2015 +0200
     3.3 @@ -23,7 +23,7 @@
     3.4        theory -> theory
     3.5    val boolean: string -> bool
     3.6    val integer: string -> int
     3.7 -  val eval_antiq: Toplevel.state -> Antiquote.antiq -> string
     3.8 +  val eval_antiquote: Toplevel.state -> Antiquote.text_antiquote -> string
     3.9    val report_text: Input.source -> unit
    3.10    val check_text: Input.source -> Toplevel.state -> unit
    3.11    val present_thy: theory -> (Toplevel.transition * Toplevel.state) list -> Token.T list -> Buffer.T
    3.12 @@ -160,48 +160,50 @@
    3.13  end;
    3.14  
    3.15  
    3.16 -(* eval_antiq *)
    3.17 +(* eval antiquotes *)
    3.18  
    3.19 -fun eval_antiq state ((ss, {range = (pos, _), ...}): Antiquote.antiq) =
    3.20 +fun read_antiquotes state source =
    3.21    let
    3.22 -    val keywords =
    3.23 -      (case try Toplevel.presentation_context_of state of
    3.24 -        SOME ctxt => Thy_Header.get_keywords' ctxt
    3.25 -      | NONE =>
    3.26 -          error ("Unknown context -- cannot expand document antiquotations" ^
    3.27 -            Position.here pos));
    3.28 +    val ants =
    3.29 +      Antiquote.read' (Input.pos_of source) (Symbol_Pos.trim_blanks (Input.source_explode source));
    3.30 +
    3.31 +    fun words (Antiquote.Text ss) = [(#1 (Symbol_Pos.range ss), Markup.words)]
    3.32 +      | words (Antiquote.Antiq _) = [];
    3.33 +    val _ = Position.reports (maps words ants);
    3.34 +  in ants end;
    3.35  
    3.36 -    val (opts, src) = Token.read_antiq keywords antiq (ss, pos);
    3.37 -    fun cmd ctxt = wrap ctxt (fn () => command src state ctxt) ();
    3.38 +fun eval_antiquote _ (Antiquote.Text ss) = Symbol_Pos.content ss
    3.39 +  | eval_antiquote state (Antiquote.Antiq (ss, {range = (pos, _), ...})) =
    3.40 +      let
    3.41 +        val keywords =
    3.42 +          (case try Toplevel.presentation_context_of state of
    3.43 +            SOME ctxt => Thy_Header.get_keywords' ctxt
    3.44 +          | NONE =>
    3.45 +              error ("Unknown context -- cannot expand document antiquotations" ^
    3.46 +                Position.here pos));
    3.47  
    3.48 -    val preview_ctxt = fold option opts (Toplevel.presentation_context_of state);
    3.49 -    val print_ctxt = Context_Position.set_visible false preview_ctxt;
    3.50 -    val _ = cmd preview_ctxt;
    3.51 -    val print_modes = space_explode "," (Config.get print_ctxt modes) @ Latex.modes;
    3.52 -  in Print_Mode.with_modes print_modes (fn () => cmd print_ctxt) () end;
    3.53 +        val (opts, src) = Token.read_antiq keywords antiq (ss, pos);
    3.54 +        fun cmd ctxt = wrap ctxt (fn () => command src state ctxt) ();
    3.55 +
    3.56 +        val preview_ctxt = fold option opts (Toplevel.presentation_context_of state);
    3.57 +        val print_ctxt = Context_Position.set_visible false preview_ctxt;
    3.58 +        val _ = cmd preview_ctxt;
    3.59 +        val print_modes = space_explode "," (Config.get print_ctxt modes) @ Latex.modes;
    3.60 +      in Print_Mode.with_modes print_modes (fn () => cmd print_ctxt) () end;
    3.61  
    3.62  
    3.63  (* check_text *)
    3.64  
    3.65 -fun eval_antiquote state source =
    3.66 -  let
    3.67 -    fun words (Antiquote.Text ss) = [(#1 (Symbol_Pos.range ss), Markup.words)]
    3.68 -      | words (Antiquote.Antiq _) = [];
    3.69 -
    3.70 -    fun expand (Antiquote.Text ss) = Symbol_Pos.content ss
    3.71 -      | expand (Antiquote.Antiq antiq) = eval_antiq state antiq;
    3.72 -
    3.73 -    val ants = Antiquote.read source;
    3.74 -    val _ = Position.reports (maps words ants);
    3.75 -  in implode (map expand ants) end;
    3.76 -
    3.77  fun report_text source =
    3.78    Position.report (Input.pos_of source) (Markup.language_document (Input.is_delimited source));
    3.79  
    3.80  fun check_text source state =
    3.81   (report_text source;
    3.82    if Toplevel.is_skipped_proof state then ()
    3.83 -  else ignore (eval_antiquote state source));
    3.84 +  else
    3.85 +    source
    3.86 +    |> read_antiquotes state
    3.87 +    |> List.app (ignore o eval_antiquote state));
    3.88  
    3.89  
    3.90  
    3.91 @@ -216,7 +218,7 @@
    3.92    | Basic_Token of Token.T
    3.93    | Markup_Token of string * Input.source
    3.94    | Markup_Env_Token of string * Input.source
    3.95 -  | Verbatim_Token of Input.source;
    3.96 +  | Raw_Token of Input.source;
    3.97  
    3.98  
    3.99  fun basic_token pred (Basic_Token tok) = pred tok
   3.100 @@ -230,22 +232,20 @@
   3.101  
   3.102  (* output token *)
   3.103  
   3.104 -val output_text =
   3.105 -  Symbol.trim_blanks #> Symbol.explode #> Latex.output_ctrl_symbols;
   3.106 -
   3.107  fun output_token state =
   3.108    let
   3.109 -    val eval = eval_antiquote state;
   3.110 +    val make_text = read_antiquotes state #> map (eval_antiquote state) #> implode;
   3.111 +    val output_text = make_text #> Symbol.explode #> Latex.output_ctrl_symbols;
   3.112      fun output No_Token = ""
   3.113        | output (Basic_Token tok) = Latex.output_token tok
   3.114        | output (Markup_Token (cmd, source)) =
   3.115 -          "%\n\\isamarkup" ^ cmd ^ "{" ^ output_text (eval source) ^ "%\n}\n"
   3.116 +          "%\n\\isamarkup" ^ cmd ^ "{" ^ output_text source ^ "%\n}\n"
   3.117        | output (Markup_Env_Token (cmd, source)) =
   3.118            "%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^
   3.119 -          output_text (eval source) ^
   3.120 +          output_text source ^
   3.121            "%\n\\end{isamarkup" ^ cmd ^ "}%\n"
   3.122 -      | output (Verbatim_Token source) =
   3.123 -          "%\n" ^ Symbol.trim_blanks (eval source) ^ "\n";
   3.124 +      | output (Raw_Token source) =
   3.125 +          "%\n" ^ output_text source ^ "\n";
   3.126    in output end;
   3.127  
   3.128  
   3.129 @@ -422,7 +422,7 @@
   3.130        (ignored ||
   3.131          markup Keyword.is_document_heading Markup_Token markup_true ||
   3.132          markup Keyword.is_document_body Markup_Env_Token markup_true ||
   3.133 -        markup Keyword.is_document_raw (Verbatim_Token o #2) "") >> single ||
   3.134 +        markup Keyword.is_document_raw (Raw_Token o #2) "") >> single ||
   3.135        command ||
   3.136        (cmt || other) >> single;
   3.137  
     4.1 --- a/src/Pure/Tools/rail.ML	Thu Oct 15 21:17:41 2015 +0200
     4.2 +++ b/src/Pure/Tools/rail.ML	Thu Oct 15 22:25:57 2015 +0200
     4.3 @@ -315,7 +315,7 @@
     4.4  
     4.5  fun output_rules state rules =
     4.6    let
     4.7 -    val output_antiq = Thy_Output.eval_antiq state;
     4.8 +    val output_antiq = Thy_Output.eval_antiquote state o Antiquote.Antiq;
     4.9      fun output_text b s =
    4.10        Output.output s
    4.11        |> b ? enclose "\\isakeyword{" "}"