src/Pure/Syntax/syntax.ML

 
 val basic_nonterms =
   (Lexicon.terminals @ [Syn_Ext.logic, "type", "types", "sort", "classes",
     Syn_Ext.args, Syn_Ext.cargs, "pttrn", "pttrns", "idt", "idts", "aprop",
     "asms", Syn_Ext.any, Syn_Ext.sprop, "num_const", "float_const",
-    "index", "struct"]);
+    "index", "struct", "id_position", "longid_position"]);
 
 
 
 (** print syntax **)
 

 val ambiguity_limit =
   Config.int (Config.declare "syntax_ambiguity_limit" (fn _ => Config.Int 10));
 
 fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos;
 
-fun read_asts ctxt (Syntax (tabs, _)) xids root (syms, pos) =
+fun read_asts ctxt (Syntax (tabs, _)) raw root (syms, pos) =
   let
     val {lexicon, gram, parse_ast_trtab, ...} = tabs;
-    val toks = Lexicon.tokenize lexicon xids syms;
+    val toks = Lexicon.tokenize lexicon raw syms;
     val _ = List.app (Lexicon.report_token ctxt) toks;
 
     val pts = Parser.parse ctxt gram root (filter Lexicon.is_proper toks)
       handle ERROR msg =>
         error (msg ^
           implode (map (Markup.markup Markup.report o Lexicon.reported_token_range ctxt) toks));
     val len = length pts;
 
     val limit = Config.get ctxt ambiguity_limit;
     fun show_pt pt =
-      Pretty.string_of (Ast.pretty_ast (Syn_Trans.parsetree_to_ast ctxt (K NONE) pt));
+      Pretty.string_of (Ast.pretty_ast (Syn_Trans.parsetree_to_ast ctxt false (K NONE) pt));
     val _ =
       if len <= Config.get ctxt ambiguity_level then ()
       else if not (Config.get ctxt ambiguity_enabled) then error (ambiguity_msg pos)
       else
         (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)") ^ ":") ::
             map show_pt (take limit pts))));
   in
-    some_results (Syn_Trans.parsetree_to_ast ctxt (lookup_tr parse_ast_trtab)) pts
+    some_results (Syn_Trans.parsetree_to_ast ctxt false (lookup_tr parse_ast_trtab)) pts
   end;
 
 
 (* read *)
 

 
 fun is_const (Syntax ({consts, ...}, _)) c = member (op =) consts c;
 
 local
 
-fun check_rule (rule as (lhs, rhs)) =
+fun check_rule rule =
   (case Ast.rule_error rule of
     SOME msg =>
       error ("Error in syntax translation rule: " ^ msg ^ "\n" ^
-        Ast.str_of_ast lhs ^ "  ->  " ^ Ast.str_of_ast rhs)
+        Pretty.string_of (Ast.pretty_rule rule))
   | NONE => rule);
 
 fun read_pattern ctxt syn (root, str) =
   let
     fun constify (ast as Ast.Constant _) = ast