# HG changeset patch
# User wenzelm
# Date 1734350139 -3600
# Node ID 26ff119fb140ca3d01d6e9609206b46aa417bd04
# Parent  b1772698bd78bfc0c7015f5b8b6c7c95f19b4bd4
clarified signature;

diff -r b1772698bd78 -r 26ff119fb140 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Sun Dec 15 22:58:48 2024 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Mon Dec 16 12:55:39 2024 +0100
@@ -52,7 +52,7 @@
   val explode_string: string * Position.T -> Symbol_Pos.T list
   val implode_str: Symbol.symbol list -> string
   val explode_str: string * Position.T -> Symbol_Pos.T list
-  val tokenize: Scan.lexicon -> bool -> Symbol_Pos.T list -> token list
+  val tokenize: Scan.lexicon -> {raw: bool} -> Symbol_Pos.T list -> token list
   val read_indexname: string -> indexname
   val read_var: string -> term
   val read_variable: string -> indexname option
@@ -312,10 +312,10 @@
   let val i = token_kind_index kind
   in fn ss => Token (i, Symbol_Pos.content ss, Symbol_Pos.range ss) end;
 
-fun tokenize lex xids syms =
+fun tokenize lex {raw} syms =
   let
-    val scan_xid =
-      (if xids then $$$ "_" @@@ scan_id || scan_id else scan_id) ||
+    val scan_id =
+      (if raw then $$$ "_" @@@ scan_id || scan_id else scan_id) ||
       $$$ "_" @@@ $$$ "_";
 
     val scan_val =
@@ -325,7 +325,7 @@
       Symbol_Pos.scan_float >> token Float ||
       scan_num >> token Num ||
       scan_longid >> token Long_Ident ||
-      scan_xid >> token Ident;
+      scan_id >> token Ident;
 
     val scan_lit = Scan.literal lex >> token Literal;
 
diff -r b1772698bd78 -r 26ff119fb140 src/Pure/Syntax/simple_syntax.ML
--- a/src/Pure/Syntax/simple_syntax.ML	Sun Dec 15 22:58:48 2024 +0100
+++ b/src/Pure/Syntax/simple_syntax.ML	Mon Dec 16 12:55:39 2024 +0100
@@ -22,7 +22,7 @@
 fun read scan s =
   (case
       Symbol_Pos.explode0 s |>
-      Lexicon.tokenize lexicon false |>
+      Lexicon.tokenize lexicon {raw = false} |>
       filter Lexicon.is_proper |>
       Scan.read Lexicon.stopper scan of
     SOME x => x
diff -r b1772698bd78 -r 26ff119fb140 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sun Dec 15 22:58:48 2024 +0100
+++ b/src/Pure/Syntax/syntax.ML	Mon Dec 16 12:55:39 2024 +0100
@@ -85,7 +85,7 @@
   val get_consts: syntax -> string -> string list
   val is_const: syntax -> string -> bool
   val is_keyword: syntax -> string -> bool
-  val tokenize: syntax -> bool -> Symbol_Pos.T list -> Lexicon.token list
+  val tokenize: syntax -> {raw: bool} -> Symbol_Pos.T list -> Lexicon.token list
   val parse: syntax -> string -> Lexicon.token list -> Parser.tree list
   val parse_ast_translation: syntax -> string -> (Proof.context -> Ast.ast list -> Ast.ast) option
   val parse_rules: syntax -> string -> (Ast.ast * Ast.ast) list
diff -r b1772698bd78 -r 26ff119fb140 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Sun Dec 15 22:58:48 2024 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Mon Dec 16 12:55:39 2024 +0100
@@ -373,7 +373,7 @@
     val syn = Proof_Context.syntax_of ctxt;
     val tr = Syntax.parse_translation syn;
     val normalize = Ast.normalize ctxt {permissive_constraints = false} (Syntax.parse_rules syn);
-    val (ambig_msgs, asts) = parse_asts ctxt false root input;
+    val (ambig_msgs, asts) = parse_asts ctxt {raw = false} root input;
     val results = (map o apsnd o Exn.maps_res) (normalize #> Exn.result (ast_to_term ctxt tr)) asts;
   in (ambig_msgs, results) end;
 
@@ -493,7 +493,7 @@
     val pos = Input.pos_of source;
     val syms = Input.source_explode source;
     val ast =
-      parse_asts ctxt true root (syms, pos)
+      parse_asts ctxt {raw = true} root (syms, pos)
       |> uncurry (report_result ctxt pos)
       |> decode [];
     val _ = Context_Position.reports_text ctxt (! reports);