tuned signature -- prefer Input.source;
authorwenzelm
Sun Nov 30 12:46:16 2014 +0100 (2014-11-30)
changeset 590658ce02aafc363
parent 59064 a8bcb5a446c8
child 59066 45ab32a542fe
tuned signature -- prefer Input.source;
src/Pure/General/antiquote.ML
src/Pure/Thy/latex.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/General/antiquote.ML	Sun Nov 30 12:24:56 2014 +0100
     1.2 +++ b/src/Pure/General/antiquote.ML	Sun Nov 30 12:46:16 2014 +0100
     1.3 @@ -14,7 +14,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 -> Symbol_Pos.T list antiquote * Symbol_Pos.T list
     1.7 -  val read: Symbol_Pos.T list * Position.T -> Symbol_Pos.T list antiquote list
     1.8 +  val read: Input.source -> Symbol_Pos.T list antiquote list
     1.9  end;
    1.10  
    1.11  structure Antiquote: ANTIQUOTE =
    1.12 @@ -75,9 +75,10 @@
    1.13  
    1.14  (* read *)
    1.15  
    1.16 -fun read (syms, pos) =
    1.17 -  (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote) syms of
    1.18 +fun read source =
    1.19 +  (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote) (Input.source_explode source) of
    1.20      SOME xs => (Position.reports_text (antiquote_reports (K []) xs); xs)
    1.21 -  | NONE => error ("Malformed quotation/antiquotation source" ^ Position.here pos));
    1.22 +  | NONE =>
    1.23 +      error ("Malformed quotation/antiquotation source" ^ Position.here (Input.pos_of source)));
    1.24  
    1.25  end;
     2.1 --- a/src/Pure/Thy/latex.ML	Sun Nov 30 12:24:56 2014 +0100
     2.2 +++ b/src/Pure/Thy/latex.ML	Sun Nov 30 12:46:16 2014 +0100
     2.3 @@ -132,8 +132,7 @@
     2.4        enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
     2.5      else if Token.is_kind Token.Verbatim tok then
     2.6        let
     2.7 -        val source = Token.source_position_of tok;
     2.8 -        val ants = Antiquote.read (Input.source_explode source, Input.pos_of source);
     2.9 +        val ants = Antiquote.read (Token.source_position_of tok);
    2.10          val out = implode (map output_syms_antiq ants);
    2.11        in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
    2.12      else if Token.is_kind Token.Cartouche tok then
     3.1 --- a/src/Pure/Thy/thy_output.ML	Sun Nov 30 12:24:56 2014 +0100
     3.2 +++ b/src/Pure/Thy/thy_output.ML	Sun Nov 30 12:46:16 2014 +0100
     3.3 @@ -180,7 +180,7 @@
     3.4  
     3.5  (* check_text *)
     3.6  
     3.7 -fun eval_antiquote state (txt, pos) =
     3.8 +fun eval_antiquote state source =
     3.9    let
    3.10      fun words (Antiquote.Text ss) = [(#1 (Symbol_Pos.range ss), Markup.words)]
    3.11        | words (Antiquote.Antiq _) = [];
    3.12 @@ -188,14 +188,14 @@
    3.13      fun expand (Antiquote.Text ss) = Symbol_Pos.content ss
    3.14        | expand (Antiquote.Antiq antiq) = eval_antiq state antiq;
    3.15  
    3.16 -    val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
    3.17 +    val ants = Antiquote.read source;
    3.18      val _ = Position.reports (maps words ants);
    3.19    in implode (map expand ants) end;
    3.20  
    3.21  fun check_text source state =
    3.22   (Position.report (Input.pos_of source) (Markup.language_document (Input.is_delimited source));
    3.23    if Toplevel.is_skipped_proof state then ()
    3.24 -  else ignore (eval_antiquote state (Input.text_of source, Input.pos_of source)));
    3.25 +  else ignore (eval_antiquote state source));
    3.26  
    3.27  
    3.28  
    3.29 @@ -206,22 +206,22 @@
    3.30  (* presentation tokens *)
    3.31  
    3.32  datatype token =
    3.33 -    NoToken
    3.34 -  | BasicToken of Token.T
    3.35 -  | MarkupToken of string * (string * Position.T)
    3.36 -  | MarkupEnvToken of string * (string * Position.T)
    3.37 -  | VerbatimToken of string * Position.T;
    3.38 +    No_Token
    3.39 +  | Basic_Token of Token.T
    3.40 +  | Markup_Token of string * Input.source
    3.41 +  | Markup_Env_Token of string * Input.source
    3.42 +  | Verbatim_Token of Input.source;
    3.43  
    3.44  fun output_token state =
    3.45    let val eval = eval_antiquote state in
    3.46 -    fn NoToken => ""
    3.47 -     | BasicToken tok => Latex.output_basic tok
    3.48 -     | MarkupToken (cmd, txt) => Latex.output_markup cmd (eval txt)
    3.49 -     | MarkupEnvToken (cmd, txt) => Latex.output_markup_env cmd (eval txt)
    3.50 -     | VerbatimToken txt => Latex.output_verbatim (eval txt)
    3.51 +    fn No_Token => ""
    3.52 +     | Basic_Token tok => Latex.output_basic tok
    3.53 +     | Markup_Token (cmd, source) => Latex.output_markup cmd (eval source)
    3.54 +     | Markup_Env_Token (cmd, source) => Latex.output_markup_env cmd (eval source)
    3.55 +     | Verbatim_Token source => Latex.output_verbatim (eval source)
    3.56    end;
    3.57  
    3.58 -fun basic_token pred (BasicToken tok) = pred tok
    3.59 +fun basic_token pred (Basic_Token tok) = pred tok
    3.60    | basic_token _ _ = false;
    3.61  
    3.62  val improper_token = basic_token Token.is_improper;
    3.63 @@ -369,7 +369,7 @@
    3.64      (* tokens *)
    3.65  
    3.66      val ignored = Scan.state --| ignore
    3.67 -      >> (fn d => (NONE, (NoToken, ("", d))));
    3.68 +      >> (fn d => (NONE, (No_Token, ("", d))));
    3.69  
    3.70      fun markup pred mk flag = Scan.peek (fn d =>
    3.71        improper |--
    3.72 @@ -378,38 +378,35 @@
    3.73        Scan.repeat tag --
    3.74        Parse.!!!! ((improper -- locale -- improper) |-- Parse.document_source --| improper_end)
    3.75        >> (fn (((tok, pos'), tags), source) =>
    3.76 -        let
    3.77 -          val name = Token.content_of tok;
    3.78 -          val text = Input.text_of source;
    3.79 -          val pos = Input.pos_of source;
    3.80 -        in (SOME (name, pos', tags), (mk (name, (text, pos)), (flag, d))) end));
    3.81 +        let val name = Token.content_of tok
    3.82 +        in (SOME (name, pos', tags), (mk (name, source), (flag, d))) end));
    3.83  
    3.84      val command = Scan.peek (fn d =>
    3.85        Parse.position (Scan.one (Token.is_command)) --
    3.86        Scan.repeat tag
    3.87        >> (fn ((tok, pos), tags) =>
    3.88          let val name = Token.content_of tok
    3.89 -        in (SOME (name, pos, tags), (BasicToken tok, (Latex.markup_false, d))) end));
    3.90 +        in (SOME (name, pos, tags), (Basic_Token tok, (Latex.markup_false, d))) end));
    3.91  
    3.92      val cmt = Scan.peek (fn d =>
    3.93 -      Parse.$$$ "--" |-- Parse.!!!! (improper |-- Parse.document_source) >> (fn source =>
    3.94 -        (NONE, (MarkupToken ("cmt", (Input.text_of source, Input.pos_of source)), ("", d)))));
    3.95 +      Parse.$$$ "--" |-- Parse.!!!! (improper |-- Parse.document_source) >>
    3.96 +        (fn source => (NONE, (Markup_Token ("cmt", source), ("", d)))));
    3.97  
    3.98      val other = Scan.peek (fn d =>
    3.99 -       Parse.not_eof >> (fn tok => (NONE, (BasicToken tok, ("", d)))));
   3.100 +       Parse.not_eof >> (fn tok => (NONE, (Basic_Token tok, ("", d)))));
   3.101  
   3.102      val token =
   3.103        ignored ||
   3.104 -      markup Keyword.is_document_heading MarkupToken Latex.markup_true ||
   3.105 -      markup Keyword.is_document_body MarkupEnvToken Latex.markup_true ||
   3.106 -      markup Keyword.is_document_raw (VerbatimToken o #2) "" ||
   3.107 +      markup Keyword.is_document_heading Markup_Token Latex.markup_true ||
   3.108 +      markup Keyword.is_document_body Markup_Env_Token Latex.markup_true ||
   3.109 +      markup Keyword.is_document_raw (Verbatim_Token o #2) "" ||
   3.110        command || cmt || other;
   3.111  
   3.112  
   3.113      (* spans *)
   3.114  
   3.115 -    val is_eof = fn (_, (BasicToken x, _)) => Token.is_eof x | _ => false;
   3.116 -    val stopper = Scan.stopper (K (NONE, (BasicToken Token.eof, ("", 0)))) is_eof;
   3.117 +    val is_eof = fn (_, (Basic_Token x, _)) => Token.is_eof x | _ => false;
   3.118 +    val stopper = Scan.stopper (K (NONE, (Basic_Token Token.eof, ("", 0)))) is_eof;
   3.119  
   3.120      val cmd = Scan.one (is_some o fst);
   3.121      val non_cmd = Scan.one (is_none o fst andf not o is_eof) >> #2;