src/Pure/Tools/rail.ML

--- a/src/Pure/Tools/rail.ML	Fri Sep 26 15:05:11 2014 +0200
+++ b/src/Pure/Tools/rail.ML	Fri Sep 26 15:10:02 2014 +0200
@@ -36,6 +36,11 @@
 fun pos_of (Token ((pos, _), _)) = pos;
 fun end_pos_of (Token ((_, pos), _)) = pos;
 
+fun range_of (toks as tok :: _) =
+      let val pos' = end_pos_of (List.last toks)
+      in Position.range (pos_of tok) pos' end
+  | range_of [] = Position.no_range;
+
 fun kind_of (Token (_, (k, _))) = k;
 fun content_of (Token (_, (_, x))) = x;
 
@@ -80,6 +85,9 @@
 
 fun token k ss = [Token (Symbol_Pos.range ss, (k, Symbol_Pos.content ss))];
 
+fun antiq_token (antiq as (ss, {range, ...})) =
+  [Token (range, (Antiq antiq, Symbol_Pos.content ss))];
+
 val scan_space = Scan.many1 (Symbol.is_blank o Symbol_Pos.symbol);
 
 val scan_keyword =
@@ -89,7 +97,7 @@
 
 val scan_token =
   scan_space >> K [] ||
-  Antiquote.scan_antiq >> (fn antiq as (ss, _) => token (Antiq antiq) ss) ||
+  Antiquote.scan_antiq >> antiq_token ||
   scan_keyword >> (token Keyword o single) ||
   Lexicon.scan_id >> token Ident ||
   Symbol_Pos.scan_string_q err_prefix >> (fn (pos1, (ss, pos2)) =>
@@ -110,6 +118,8 @@
 
 (** parsing **)
 
+(* parser combinators *)
+
 fun !!! scan =
   let
     val prefix = "Rail syntax error";
@@ -140,6 +150,78 @@
 
 val antiq = Scan.some (fn tok => (case kind_of tok of Antiq a => SOME a | _ => NONE));
 
+fun RANGE scan = Scan.trace scan >> apsnd range_of;
+fun RANGE_APP scan = RANGE scan >> (fn (f, r) => f r);
+
+
+(* parse trees *)
+
+datatype trees =
+  CAT of tree list * Position.range
+and tree =
+  BAR of trees list * Position.range |
+  STAR of (trees * trees) * Position.range |
+  PLUS of (trees * trees) * Position.range |
+  MAYBE of tree * Position.range |
+  NEWLINE of Position.range |
+  NONTERMINAL of string * Position.range |
+  TERMINAL of (bool * string) * Position.range |
+  ANTIQUOTE of (bool * Antiquote.antiq) * Position.range;
+
+fun reports_of_tree ctxt =
+  if Context_Position.is_visible ctxt then
+    let
+      fun reports r =
+        if r = Position.no_range then []
+        else [(Position.set_range r, Markup.expression)];
+      fun trees (CAT (ts, r)) = reports r @ maps tree ts
+      and tree (BAR (Ts, r)) = reports r @ maps trees Ts
+        | tree (STAR ((T1, T2), r)) = reports r @ trees T1 @ trees T2
+        | tree (PLUS ((T1, T2), r)) = reports r @ trees T1 @ trees T2
+        | tree (MAYBE (t, r)) = reports r @ tree t
+        | tree (NEWLINE r) = reports r
+        | tree (NONTERMINAL (_, r)) = reports r
+        | tree (TERMINAL (_, r)) = reports r
+        | tree (ANTIQUOTE (_, r)) = reports r;
+    in distinct (op =) o tree end
+  else K [];
+
+local
+
+val at_mode = Scan.option ($$$ "@") >> (fn NONE => false | _ => true);
+
+fun body x = (RANGE (enum1 "|" body1) >> BAR) x
+and body0 x = (RANGE (enum "|" body1) >> BAR) x
+and body1 x =
+ (RANGE_APP (body2 :|-- (fn a =>
+   $$$ "*" |-- !!! body4e >> (fn b => fn r => CAT ([STAR ((a, b), r)], r)) ||
+   $$$ "+" |-- !!! body4e >> (fn b => fn r => CAT ([PLUS ((a, b), r)], r)) ||
+   Scan.succeed (K a)))) x
+and body2 x = (RANGE (Scan.repeat1 body3) >> CAT) x
+and body3 x =
+ (RANGE_APP (body4 :|-- (fn a =>
+   $$$ "?" >> K (curry MAYBE a) ||
+   Scan.succeed (K a)))) x
+and body4 x =
+ ($$$ "(" |-- !!! (body0 --| $$$ ")") ||
+  RANGE_APP
+   ($$$ "\<newline>" >> K NEWLINE ||
+    ident >> curry NONTERMINAL ||
+    at_mode -- string >> curry TERMINAL ||
+    at_mode -- antiq >> curry ANTIQUOTE)) x
+and body4e x =
+  (RANGE (Scan.option body4) >> (fn (a, r) => CAT (the_list a, r))) x;
+
+val rule_name = ident >> Antiquote.Text || antiq >> Antiquote.Antiq;
+val rule = rule_name -- ($$$ ":" |-- !!! body) || body >> pair (Antiquote.Text "");
+val rules = enum1 ";" (Scan.option rule) >> map_filter I;
+
+in
+
+fun parse_rules toks =
+  #1 (Scan.error (Scan.finite stopper (rules --| !!! (Scan.ahead (Scan.one is_eof)))) toks);
+
+end;
 
 
 (** rail expressions **)
@@ -156,68 +238,58 @@
   Terminal of bool * string |
   Antiquote of bool * Antiquote.antiq;
 
-fun reverse_cat (Cat (y, rails)) = Cat (y, rev (map reverse rails))
-and reverse (Bar cats) = Bar (map reverse_cat cats)
-  | reverse (Plus (cat1, cat2)) = Plus (reverse_cat cat1, reverse_cat cat2)
-  | reverse x = x;
+fun is_newline (Newline _) = true | is_newline _ = false;
+
+
+(* prepare *)
+
+local
 
 fun cat rails = Cat (0, rails);
 
 val empty = cat [];
 fun is_empty (Cat (_, [])) = true | is_empty _ = false;
 
-fun is_newline (Newline _) = true | is_newline _ = false;
-
 fun bar [Cat (_, [rail])] = rail
   | bar cats = Bar cats;
 
-fun plus cat1 cat2 = Plus (cat1, reverse_cat cat2);
+fun reverse_cat (Cat (y, rails)) = Cat (y, rev (map reverse rails))
+and reverse (Bar cats) = Bar (map reverse_cat cats)
+  | reverse (Plus (cat1, cat2)) = Plus (reverse_cat cat1, reverse_cat cat2)
+  | reverse x = x;
+
+fun plus (cat1, cat2) = Plus (cat1, reverse_cat cat2);
+
+in
 
-fun star cat1 cat2 =
-  if is_empty cat2 then plus empty cat1
-  else bar [empty, cat [plus cat1 cat2]];
+fun prepare_trees (CAT (ts, _)) = Cat (0, map prepare_tree ts)
+and prepare_tree (BAR (Ts, _)) = bar (map prepare_trees Ts)
+  | prepare_tree (STAR (Ts, _)) =
+      let val (cat1, cat2) = pairself prepare_trees Ts in
+        if is_empty cat2 then plus (empty, cat1)
+        else bar [empty, cat [plus (cat1, cat2)]]
+      end
+  | prepare_tree (PLUS (Ts, _)) = plus (pairself prepare_trees Ts)
+  | prepare_tree (MAYBE (t, _)) = bar [empty, cat [prepare_tree t]]
+  | prepare_tree (NEWLINE _) = Newline 0
+  | prepare_tree (NONTERMINAL (a, _)) = Nonterminal a
+  | prepare_tree (TERMINAL (a, _)) = Terminal a
+  | prepare_tree (ANTIQUOTE (a, _)) = Antiquote a;
 
-fun maybe rail = bar [empty, cat [rail]];
+end;
 
 
 (* read *)
 
-local
-
-val at_mode = Scan.option ($$$ "@") >> (fn NONE => false | _ => true);
-
-fun body x = (enum1 "|" body1 >> bar) x
-and body0 x = (enum "|" body1 >> bar) x
-and body1 x =
- (body2 :|-- (fn a =>
-   $$$ "*" |-- !!! body4e >> (cat o single o star a) ||
-   $$$ "+" |-- !!! body4e >> (cat o single o plus a) ||
-   Scan.succeed a)) x
-and body2 x = (Scan.repeat1 body3 >> cat) x
-and body3 x = (body4 :|-- (fn a => $$$ "?" >> K (maybe a) || Scan.succeed a)) x
-and body4 x =
- ($$$ "(" |-- !!! (body0 --| $$$ ")") ||
-  $$$ "\<newline>" >> K (Newline 0) ||
-  ident >> Nonterminal ||
-  at_mode -- string >> Terminal ||
-  at_mode -- antiq >> Antiquote) x
-and body4e x = (Scan.option body4 >> (cat o the_list)) x;
-
-val rule_name = ident >> Antiquote.Text || antiq >> Antiquote.Antiq;
-val rule = rule_name -- ($$$ ":" |-- !!! body) || body >> pair (Antiquote.Text "");
-val rules = enum1 ";" (Scan.option rule) >> map_filter I;
-
-in
-
 fun read ctxt (source: Symbol_Pos.source) =
   let
     val {text, pos, ...} = source;
     val _ = Context_Position.report ctxt pos Markup.language_rail;
     val toks = tokenize (Symbol_Pos.explode (text, pos));
     val _ = Context_Position.reports ctxt (maps reports_of_token toks);
-  in #1 (Scan.error (Scan.finite stopper (rules --| !!! (Scan.ahead (Scan.one is_eof)))) toks) end;
-
-end;
+    val rules = parse_rules toks;
+    val _ = Position.reports (maps (reports_of_tree ctxt o #2) rules);
+  in map (apsnd prepare_tree) rules end;
 
 
 (* latex output *)