# HG changeset patch
# User wenzelm
# Date 1734191933 -3600
# Node ID fcf44ef51057269c2574b6dcca8f0c6ed373f0db
# Parent  81a72b7fcb0cce61d0385eaf423383411e68a044
clarified signature and modules;

diff -r 81a72b7fcb0c -r fcf44ef51057 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Fri Dec 13 23:23:07 2024 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Sat Dec 14 16:58:53 2024 +0100
@@ -98,15 +98,7 @@
 
 (* translation rules *)
 
-fun read_trrules thy raw_rules =
-  let
-    val ctxt = Proof_Context.init_global thy;
-    val read_root =
-      dest_Type_name o Proof_Context.read_type_name {proper = true, strict = false} ctxt;
-  in
-    raw_rules
-    |> map (Syntax.map_trrule (fn (r, s) => Syntax_Phases.parse_ast_pattern ctxt (read_root r, s)))
-  end;
+val read_trrules = map o Syntax.parse_trrule o Proof_Context.init_global;
 
 fun translations args thy = Sign.add_trrules (read_trrules thy args) thy;
 fun no_translations args thy = Sign.del_trrules (read_trrules thy args) thy;
diff -r 81a72b7fcb0c -r fcf44ef51057 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Fri Dec 13 23:23:07 2024 +0100
+++ b/src/Pure/Syntax/syntax.ML	Sat Dec 14 16:58:53 2024 +0100
@@ -7,6 +7,10 @@
 
 signature SYNTAX =
 sig
+  datatype 'a trrule =
+    Parse_Rule of 'a * 'a |
+    Print_Rule of 'a * 'a |
+    Parse_Print_Rule of 'a * 'a
   type operations
   val install_operations: operations -> theory -> theory
   val root: string Config.T
@@ -18,6 +22,7 @@
   val read_input: string -> Input.source
   val parse_input: Proof.context -> (XML.tree list -> 'a) ->
     (bool -> Markup.T) -> (Symbol_Pos.T list * Position.T -> 'a) -> string -> 'a
+  val parse_trrule: Proof.context -> (string * string) trrule -> Ast.ast trrule
   val parse_sort: Proof.context -> string -> sort
   val parse_typ: Proof.context -> string -> typ
   val parse_term: Proof.context -> string -> term
@@ -100,10 +105,6 @@
   val print_gram: syntax -> unit
   val print_trans: syntax -> unit
   val print_syntax: syntax -> unit
-  datatype 'a trrule =
-    Parse_Rule of 'a * 'a |
-    Print_Rule of 'a * 'a |
-    Parse_Print_Rule of 'a * 'a
   val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
   val update_trfuns: Proof.context ->
     (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
@@ -134,8 +135,14 @@
 
 (* operations *)
 
+datatype 'a trrule =
+  Parse_Rule of 'a * 'a |
+  Print_Rule of 'a * 'a |
+  Parse_Print_Rule of 'a * 'a;
+
 type operations =
- {parse_sort: Proof.context -> string -> sort,
+ {parse_trrule: Proof.context -> (string * string) trrule -> Ast.ast trrule,
+  parse_sort: Proof.context -> string -> sort,
   parse_typ: Proof.context -> string -> typ,
   parse_term: Proof.context -> string -> term,
   parse_prop: Proof.context -> string -> term,
@@ -233,6 +240,7 @@
 
 (* (un)parsing *)
 
+val parse_trrule = operation #parse_trrule;
 val parse_sort = operation #parse_sort;
 val parse_typ = operation #parse_typ;
 val parse_term = operation #parse_term;
@@ -717,11 +725,6 @@
 
 (* rules *)
 
-datatype 'a trrule =
-  Parse_Rule of 'a * 'a |
-  Print_Rule of 'a * 'a |
-  Parse_Print_Rule of 'a * 'a;
-
 fun map_trrule f (Parse_Rule (x, y)) = Parse_Rule (f x, f y)
   | map_trrule f (Print_Rule (x, y)) = Print_Rule (f x, f y)
   | map_trrule f (Parse_Print_Rule (x, y)) = Parse_Print_Rule (f x, f y);
diff -r 81a72b7fcb0c -r fcf44ef51057 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Fri Dec 13 23:23:07 2024 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Sat Dec 14 16:58:53 2024 +0100
@@ -13,7 +13,6 @@
   val decode_typ: term -> typ
   val decode_term: Proof.context ->
     Position.report_text list * term Exn.result -> Position.report_text list * term Exn.result
-  val parse_ast_pattern: Proof.context -> string * string -> Ast.ast
   val term_of_typ: Proof.context -> typ -> term
   val print_checks: Proof.context -> unit
   val typ_check: int -> string -> (Proof.context -> typ list -> typ list) ->
@@ -459,10 +458,14 @@
   end;
 
 
-(* parse_ast_pattern *)
+(* translation rules *)
 
-fun parse_ast_pattern ctxt (root, str) =
+fun parse_trrule ctxt = Syntax.map_trrule (fn (raw_root, raw_pattern) =>
   let
+    val root = raw_root
+      |> Proof_Context.read_type_name {proper = true, strict = false} ctxt
+      |> dest_Type_name;
+
     val syn = Proof_Context.syntax_of ctxt;
 
     val reports = Unsynchronized.ref ([]: Position.report_text list);
@@ -486,7 +489,7 @@
           else decode_appl ps asts
       | decode ps (Ast.Appl asts) = decode_appl ps asts;
 
-    val source = Syntax.read_input str;
+    val source = Syntax.read_input raw_pattern;
     val pos = Input.pos_of source;
     val syms = Input.source_explode source;
     val ast =
@@ -494,7 +497,7 @@
       |> uncurry (report_result ctxt pos)
       |> decode [];
     val _ = Context_Position.reports_text ctxt (! reports);
-  in ast end;
+  in ast end);
 
 
 
@@ -1024,7 +1027,8 @@
 val _ =
   Theory.setup
    (Syntax.install_operations
-     {parse_sort = parse_sort,
+     {parse_trrule = parse_trrule,
+      parse_sort = parse_sort,
       parse_typ = parse_typ,
       parse_term = parse_term false,
       parse_prop = parse_term true,