# 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,