src/Pure/Tools/rail.ML
changeset 55613 ad446b45efff
parent 55526 39708e59f4b0
child 55828 42ac3cfb89f6
     1.1 --- a/src/Pure/Tools/rail.ML	Wed Feb 19 20:53:09 2014 +0100
     1.2 +++ b/src/Pure/Tools/rail.ML	Wed Feb 19 20:56:29 2014 +0100
     1.3 @@ -39,6 +39,10 @@
     1.4  
     1.5  fun print_keyword x = print_kind Keyword ^ " " ^ quote x;
     1.6  
     1.7 +fun reports_of_token (Token ((pos, _), (String, _))) = [(pos, Markup.inner_string)]
     1.8 +  | reports_of_token (Token (_, (Antiq antiq, _))) = Antiquote.antiq_reports antiq
     1.9 +  | reports_of_token _ = [];
    1.10 +
    1.11  
    1.12  (* stopper *)
    1.13  
    1.14 @@ -71,7 +75,8 @@
    1.15    Antiquote.scan_antiq >> (fn antiq as (ss, _) => token (Antiq antiq) ss) ||
    1.16    scan_keyword >> (token Keyword o single) ||
    1.17    Lexicon.scan_id >> token Ident ||
    1.18 -  Symbol_Pos.scan_string_q err_prefix >> (token String o #1 o #2);
    1.19 +  Symbol_Pos.scan_string_q err_prefix >> (fn (pos1, (ss, pos2)) =>
    1.20 +    [Token (Position.range pos1 pos2, (String, Symbol_Pos.content ss))]);
    1.21  
    1.22  val scan =
    1.23    (Scan.repeat scan_token >> flat) --|
    1.24 @@ -80,7 +85,7 @@
    1.25  
    1.26  in
    1.27  
    1.28 -val tokenize = #1 o Scan.error (Scan.finite Symbol_Pos.stopper scan) o Symbol_Pos.explode;
    1.29 +val tokenize = #1 o Scan.error (Scan.finite Symbol_Pos.stopper scan);
    1.30  
    1.31  end;
    1.32  
    1.33 @@ -187,8 +192,12 @@
    1.34  
    1.35  in
    1.36  
    1.37 -val read =
    1.38 -  #1 o Scan.error (Scan.finite stopper (rules --| !!! (Scan.ahead (Scan.one is_eof)))) o tokenize;
    1.39 +fun read ctxt (s, pos) =
    1.40 +  let
    1.41 +    val _ = Context_Position.report ctxt pos Markup.language_rail;
    1.42 +    val toks = tokenize (Symbol_Pos.explode (s, pos));
    1.43 +    val _ = Context_Position.reports ctxt (maps reports_of_token toks);
    1.44 +  in #1 (Scan.error (Scan.finite stopper (rules --| !!! (Scan.ahead (Scan.one is_eof)))) toks) end;
    1.45  
    1.46  end;
    1.47  
    1.48 @@ -267,7 +276,7 @@
    1.49  val _ = Theory.setup
    1.50    (Thy_Output.antiquotation @{binding rail}
    1.51      (Scan.lift (Parse.source_position (Parse.string || Parse.cartouche)))
    1.52 -    (fn {state, ...} => output_rules state o read));
    1.53 +    (fn {state, context, ...} => output_rules state o read context));
    1.54  
    1.55  end;
    1.56