--- a/src/Pure/Syntax/syntax.ML Fri Aug 27 18:00:45 2010 +0200
+++ b/src/Pure/Syntax/syntax.ML Fri Aug 27 19:43:28 2010 +0200
@@ -485,7 +485,7 @@
val _ = List.app (Lexicon.report_token ctxt) toks;
val root' = if root <> "prop" andalso is_logtype root then Syn_Ext.logic else root;
- val pts = Parser.parse gram root' (filter Lexicon.is_proper toks);
+ val pts = Parser.parse ctxt gram root' (filter Lexicon.is_proper toks);
val len = length pts;
val limit = ! ambiguity_limit;
@@ -495,7 +495,7 @@
if len <= ! ambiguity_level then ()
else if ! ambiguity_is_error then error (ambiguity_msg pos)
else
- (warning (cat_lines
+ (Context_Position.if_visible ctxt warning (cat_lines
(("Ambiguous input" ^ Position.str_of pos ^
"\nproduces " ^ string_of_int len ^ " parse trees" ^
(if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
@@ -519,8 +519,8 @@
(* read terms *)
(*brute-force disambiguation via type-inference*)
-fun disambig _ _ [t] = t
- | disambig pp check ts =
+fun disambig _ _ _ [t] = t
+ | disambig ctxt pp check ts =
let
val level = ! ambiguity_level;
val limit = ! ambiguity_limit;
@@ -539,7 +539,8 @@
if null results then cat_error (ambig_msg ()) (cat_lines (map_filter I errs))
else if len = 1 then
(if ambiguity > level then
- warning "Fortunately, only one parse tree is type correct.\n\
+ Context_Position.if_visible ctxt warning
+ "Fortunately, only one parse tree is type correct.\n\
\You may still want to disambiguate your grammar or your input."
else (); hd results)
else cat_error (ambig_msg ()) (cat_lines
@@ -551,7 +552,7 @@
fun standard_parse_term pp check get_sort map_const map_free ctxt is_logtype syn ty (syms, pos) =
read ctxt is_logtype syn ty (syms, pos)
|> map (Type_Ext.decode_term get_sort map_const map_free)
- |> disambig (Printer.pp_show_brackets pp) check;
+ |> disambig ctxt (Printer.pp_show_brackets pp) check;
(* read types *)