src/Pure/Syntax/syntax.ML
changeset 27786 4525c6f5d753
parent 27768 398c64b2acef
child 27803 c08f4ea29b83
     1.1 --- a/src/Pure/Syntax/syntax.ML	Thu Aug 07 22:32:01 2008 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Thu Aug 07 22:32:03 2008 +0200
     1.3 @@ -36,18 +36,20 @@
     1.4    val print_trans: syntax -> unit
     1.5    val print_syntax: syntax -> unit
     1.6    val guess_infix: syntax -> string -> mixfix option
     1.7 +  val read_token: string -> SymbolPos.T list * Position.T
     1.8    val ambiguity_is_error: bool ref
     1.9    val ambiguity_level: int ref
    1.10    val ambiguity_limit: int ref
    1.11 -  val read: Proof.context -> (string -> bool) -> syntax -> typ -> string -> term list
    1.12    val standard_parse_term: Pretty.pp -> (term -> string option) ->
    1.13      (((string * int) * sort) list -> string * int -> Term.sort) ->
    1.14      (string -> bool * string) -> (string -> string option) ->
    1.15      (typ -> typ) -> (sort -> sort) -> Proof.context ->
    1.16 -    (string -> bool) -> syntax -> typ -> string -> term
    1.17 +    (string -> bool) -> syntax -> typ -> SymbolPos.T list * Position.T -> term
    1.18    val standard_parse_typ: Proof.context -> syntax ->
    1.19 -    ((indexname * sort) list -> indexname -> sort) -> (sort -> sort) -> string -> typ
    1.20 -  val standard_parse_sort: Proof.context -> syntax -> (sort -> sort) -> string -> sort
    1.21 +    ((indexname * sort) list -> indexname -> sort) -> (sort -> sort) ->
    1.22 +    SymbolPos.T list * Position.T -> typ
    1.23 +  val standard_parse_sort: Proof.context -> syntax -> (sort -> sort) ->
    1.24 +    SymbolPos.T list * Position.T -> sort
    1.25    datatype 'a trrule =
    1.26      ParseRule of 'a * 'a |
    1.27      PrintRule of 'a * 'a |
    1.28 @@ -455,18 +457,33 @@
    1.29  
    1.30  (** read **)
    1.31  
    1.32 +(* read token -- with optional YXML encoding of position *)
    1.33 +
    1.34 +fun read_token str =
    1.35 +  let val (text, pos) =
    1.36 +    if YXML.detect str then
    1.37 +      (case YXML.parse str of
    1.38 +        XML.Elem ("token", props, [XML.Text text]) =>
    1.39 +          let val pos = Position.of_properties props;
    1.40 +          in (text, pos) end
    1.41 +      | _ => (str, Position.none))
    1.42 +    else (str, Position.none)
    1.43 +  in (SymbolPos.explode (text, pos), pos) end;
    1.44 +
    1.45 +
    1.46  (* read_ast *)
    1.47  
    1.48  val ambiguity_is_error = ref false;
    1.49  val ambiguity_level = ref 1;
    1.50  val ambiguity_limit = ref 10;
    1.51  
    1.52 -fun read_asts ctxt is_logtype (Syntax (tabs, _)) xids root str =
    1.53 +fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos;
    1.54 +
    1.55 +fun read_asts ctxt is_logtype (Syntax (tabs, _)) xids root (syms, pos) =
    1.56    let
    1.57      val {lexicon, gram, parse_ast_trtab, ...} = tabs;
    1.58      val root' = if root <> "prop" andalso is_logtype root then SynExt.logic else root;
    1.59 -    val chars = SymbolPos.explode (str, Position.none);
    1.60 -    val pts = Parser.parse gram root' (Lexicon.tokenize lexicon xids chars);
    1.61 +    val pts = Parser.parse gram root' (Lexicon.tokenize lexicon xids syms);
    1.62      val len = length pts;
    1.63  
    1.64      val limit = ! ambiguity_limit;
    1.65 @@ -474,11 +491,11 @@
    1.66        Pretty.string_of (Ast.pretty_ast (hd (SynTrans.pts_to_asts ctxt (K NONE) [pt])));
    1.67    in
    1.68      if len <= ! ambiguity_level then ()
    1.69 -    else if ! ambiguity_is_error then error ("Ambiguous input " ^ quote str)
    1.70 +    else if ! ambiguity_is_error then error (ambiguity_msg pos)
    1.71      else
    1.72        (warning (cat_lines
    1.73 -        (("Ambiguous input " ^ quote str ^ "\n" ^
    1.74 -          "produces " ^ string_of_int len ^ " parse trees" ^
    1.75 +        (("Ambiguous input " ^ Position.str_of pos ^
    1.76 +          "\nproduces " ^ string_of_int len ^ " parse trees" ^
    1.77            (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
    1.78            map show_pt (Library.take (limit, pts)))));
    1.79      SynTrans.pts_to_asts ctxt (lookup_tr parse_ast_trtab) pts
    1.80 @@ -487,10 +504,10 @@
    1.81  
    1.82  (* read *)
    1.83  
    1.84 -fun read ctxt is_logtype (syn as Syntax (tabs, _)) ty str =
    1.85 +fun read ctxt is_logtype (syn as Syntax (tabs, _)) ty inp =
    1.86    let
    1.87      val {parse_ruletab, parse_trtab, ...} = tabs;
    1.88 -    val asts = read_asts ctxt is_logtype syn false (SynExt.typ_to_nonterm ty) str;
    1.89 +    val asts = read_asts ctxt is_logtype syn false (SynExt.typ_to_nonterm ty) inp;
    1.90    in
    1.91      SynTrans.asts_to_terms ctxt (lookup_tr parse_trtab)
    1.92        (map (Ast.normalize_ast (Symtab.lookup_list parse_ruletab)) asts)
    1.93 @@ -530,26 +547,26 @@
    1.94        end;
    1.95  
    1.96  fun standard_parse_term pp check get_sort map_const map_free map_type map_sort
    1.97 -    ctxt is_logtype syn ty str =
    1.98 -  read ctxt is_logtype syn ty str
    1.99 +    ctxt is_logtype syn ty (syms, pos) =
   1.100 +  read ctxt is_logtype syn ty (syms, pos)
   1.101    |> map (TypeExt.decode_term get_sort map_const map_free map_type map_sort)
   1.102    |> disambig (Printer.pp_show_brackets pp) check;
   1.103  
   1.104  
   1.105  (* read types *)
   1.106  
   1.107 -fun standard_parse_typ ctxt syn get_sort map_sort str =
   1.108 -  (case read ctxt (K false) syn SynExt.typeT str of
   1.109 +fun standard_parse_typ ctxt syn get_sort map_sort (syms, pos) =
   1.110 +  (case read ctxt (K false) syn SynExt.typeT (syms, pos) of
   1.111      [t] => TypeExt.typ_of_term (get_sort (TypeExt.term_sorts map_sort t)) map_sort t
   1.112 -  | _ => error "read_typ: ambiguous syntax");
   1.113 +  | _ => error (ambiguity_msg pos));
   1.114  
   1.115  
   1.116  (* read sorts *)
   1.117  
   1.118 -fun standard_parse_sort ctxt syn map_sort str =
   1.119 -  (case read ctxt (K false) syn TypeExt.sortT str of
   1.120 +fun standard_parse_sort ctxt syn map_sort (syms, pos) =
   1.121 +  (case read ctxt (K false) syn TypeExt.sortT (syms, pos) of
   1.122      [t] => TypeExt.sort_of_term map_sort t
   1.123 -  | _ => error "read_sort: ambiguous syntax");
   1.124 +  | _ => error (ambiguity_msg pos));
   1.125  
   1.126  
   1.127  
   1.128 @@ -591,13 +608,13 @@
   1.129            if member (op =) consts x orelse NameSpace.is_qualified x then Ast.Constant x
   1.130            else ast
   1.131        | constify (Ast.Appl asts) = Ast.Appl (map constify asts);
   1.132 +
   1.133 +    val (syms, pos) = read_token str;
   1.134    in
   1.135 -    (case read_asts ctxt is_logtype syn true root str of
   1.136 +    (case read_asts ctxt is_logtype syn true root (syms, pos) of
   1.137        [ast] => constify ast
   1.138 -    | _ => error ("Syntactically ambiguous input: " ^ quote str))
   1.139 -  end handle ERROR msg =>
   1.140 -    cat_error msg ("The error(s) above occurred in translation pattern " ^
   1.141 -      quote str);
   1.142 +    | _ => error (ambiguity_msg pos))
   1.143 +  end;
   1.144  
   1.145  fun prep_rules rd_pat raw_rules =
   1.146    let val rules = map (map_trrule rd_pat) raw_rules in