# HG changeset patch # User wenzelm # Date 1727012779 -7200 # Node ID bbe2c56fe255f9dba59fd8ce4d516fcb069710f2 # Parent 1a52cc1c327440a6b8d1c50eb09bf73d7e1eb3fa more uniform treatment of Markup.notation and Markup.expression: manage kinds via context; diff -r 1a52cc1c3274 -r bbe2c56fe255 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Sun Sep 22 14:41:34 2024 +0200 +++ b/src/Pure/PIDE/markup.ML Sun Sep 22 15:46:19 2024 +0200 @@ -67,13 +67,7 @@ val position_properties: string list val position_property: Properties.entry -> bool val def_name: string -> string - val notation_mixfixN: string - val notation_prefixN: string - val notation_postfixN: string - val notation_infixN: string - val notation_binderN: string - val notations: string list - val notationN: string val notation: {kind: string, name: string} -> T + val notationN: string val notation: string -> T val notation0: T val expressionN: string val expression: string -> T val expression0: T @@ -442,18 +436,10 @@ | NONE => make_def a); -(* notation: mixfix annotations *) - -val notation_mixfixN = "mixfix"; -val notation_prefixN = "prefix"; -val notation_postfixN = "postfix"; -val notation_infixN = "infix"; -val notation_binderN = "binder"; -val notations = - [notation_mixfixN, notation_prefixN, notation_postfixN, notation_infixN, notation_binderN]; +(* notation -- inner syntax clause *) val notationN = "notation"; -fun notation {kind, name} = (notationN, kind_proper kind @ name_proper name); +fun notation kind = (notationN, kind_proper kind); val notation0 = (notationN, []); diff -r 1a52cc1c3274 -r bbe2c56fe255 src/Pure/PIDE/markup_kind.ML --- a/src/Pure/PIDE/markup_kind.ML Sun Sep 22 14:41:34 2024 +0200 +++ b/src/Pure/PIDE/markup_kind.ML Sun Sep 22 15:46:19 2024 +0200 @@ -1,15 +1,26 @@ (* Title: Pure/markup_kind.ML Author: Makarius -Formally defined kind for Markup.expression. +Formally defined kind for Markup.notation and Markup.expression. *) signature MARKUP_KIND = sig + val get_notation_kinds: Proof.context -> string list + val check_notation_kind: Proof.context -> xstring * Position.T -> string + val setup_notation_kind: binding -> theory -> string * theory + val check_notation: Proof.context -> xstring * Position.T -> Markup.T + val setup_notation: binding -> Markup.T + val get_expression_kinds: Proof.context -> string list val check_expression_kind: Proof.context -> xstring * Position.T -> string val setup_expression_kind: binding -> theory -> string * theory val check_expression: Proof.context -> xstring * Position.T -> Markup.T val setup_expression: binding -> Markup.T + val markup_mixfix: Markup.T + val markup_prefix: Markup.T + val markup_postfix: Markup.T + val markup_infix: Markup.T + val markup_binder: Markup.T val markup_type: Markup.T val markup_type_application: Markup.T val markup_term: Markup.T @@ -27,34 +38,70 @@ structure Data = Theory_Data ( - type T = unit Name_Space.table; - val empty : T = Name_Space.empty_table "markup_expression_kind"; - fun merge data : T = Name_Space.merge_tables data; + type T = unit Name_Space.table * unit Name_Space.table; + val empty : T = + (Name_Space.empty_table "markup_notation_kind", + Name_Space.empty_table "markup_expression_kind"); + fun merge ((tab1, tab2), (tab1', tab2')) : T = + (Name_Space.merge_tables (tab1, tab1'), + Name_Space.merge_tables (tab2, tab2')); ); (* kind *) -fun check_expression_kind ctxt = - Name_Space.check (Context.Proof ctxt) (Data.get (Proof_Context.theory_of ctxt)) #> #1; +local -fun setup_expression_kind binding thy = +fun get_kinds which ctxt = + which (Data.get (Proof_Context.theory_of ctxt)) + |> Name_Space.dest_table + |> map #1 + |> sort_strings; + +fun check_kind which ctxt = + Name_Space.check (Context.Proof ctxt) (which (Data.get (Proof_Context.theory_of ctxt))) #> #1; + +fun setup_kind which ap binding thy = let val context = Name_Space.map_naming (K Name_Space.global_naming) (Context.Theory thy); - val (name, data') = Name_Space.define context true (binding, ()) (Data.get thy); - in (name, Data.put data' thy) end; + val (name, tab') = Name_Space.define context true (binding, ()) (which (Data.get thy)); + in (name, (Data.map o ap) (K tab') thy) end; + +in + +val get_notation_kinds = get_kinds #1; +val get_expression_kinds = get_kinds #2; + +val check_notation_kind = check_kind #1; +val check_expression_kind = check_kind #2; + +val setup_notation_kind = setup_kind #1 apfst; +val setup_expression_kind = setup_kind #2 apsnd; + +end; (* markup *) +fun check_notation ctxt = check_notation_kind ctxt #> Markup.notation; + fun check_expression ctxt = check_expression_kind ctxt #> Markup.expression; +fun setup_notation binding = + Context.>>> (Context.map_theory_result (setup_notation_kind binding #>> Markup.notation)); + fun setup_expression binding = Context.>>> (Context.map_theory_result (setup_expression_kind binding #>> Markup.expression)); (* concrete markup *) +val markup_mixfix = setup_notation (Binding.make ("mixfix", \<^here>)); +val markup_prefix = setup_notation (Binding.make ("prefix", \<^here>)); +val markup_postfix = setup_notation (Binding.make ("postfix", \<^here>)); +val markup_infix = setup_notation (Binding.make ("infix", \<^here>)); +val markup_binder = setup_notation (Binding.make ("binder", \<^here>)); + val markup_type = setup_expression (Binding.make ("type", \<^here>)); val markup_type_application = setup_expression (Binding.make ("type_application", \<^here>)); diff -r 1a52cc1c3274 -r bbe2c56fe255 src/Pure/Syntax/mixfix.ML --- a/src/Pure/Syntax/mixfix.ML Sun Sep 22 14:41:34 2024 +0200 +++ b/src/Pure/Syntax/mixfix.ML Sun Sep 22 15:46:19 2024 +0200 @@ -160,13 +160,11 @@ val infix_arg1 = Symbol_Pos.explode0 "_ "; val infix_arg2 = Symbol_Pos.explode0 "/ _)"; -fun infix_block ctxt ss = - Syntax_Ext.make_notation - {kind = Markup.notation_infixN, - name = Syntax_Ext.mfix_name ctxt ss} - |> cartouche - |> Symbol_Pos.explode0 - |> append infix_bg; +fun infix_block ctxt = + Syntax_Ext.mfix_name ctxt #> + Syntax_Ext.block_annotation 0 Markup_Kind.markup_infix #> + Symbol_Pos.explode0 #> + append infix_bg; (* binder notation *) @@ -177,15 +175,11 @@ val binder_bg = Symbol_Pos.explode0 "("; val binder_en = Symbol_Pos.explode0 "_./ _)"; -fun binder_block ctxt ss = - implode_space - ["indent=3", - Syntax_Ext.make_notation - {kind = Markup.notation_binderN, - name = Syntax_Ext.mfix_name ctxt ss}] - |> cartouche - |> Symbol_Pos.explode0 - |> append binder_bg; +fun binder_block ctxt = + Syntax_Ext.mfix_name ctxt #> + Syntax_Ext.block_annotation 3 Markup_Kind.markup_binder #> + Symbol_Pos.explode0 #> + append binder_bg; fun binder_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) = [Type ("idts", []), ty2] ---> ty3 diff -r 1a52cc1c3274 -r bbe2c56fe255 src/Pure/Syntax/syntax_ext.ML --- a/src/Pure/Syntax/syntax_ext.ML Sun Sep 22 14:41:34 2024 +0200 +++ b/src/Pure/Syntax/syntax_ext.ML Sun Sep 22 15:46:19 2024 +0200 @@ -29,7 +29,7 @@ print_translation: (string * ((Proof.context -> typ -> term list -> term) * stamp)) list, print_rules: (Ast.ast * Ast.ast) list, print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list} - val make_notation: {kind: string, name: string} -> string + val block_annotation: int -> Markup.T -> string -> string val mfix_name: Proof.context -> Symbol_Pos.T list -> string val mfix_args: Proof.context -> Symbol_Pos.T list -> int val mixfix_args: Proof.context -> Input.source -> int @@ -123,8 +123,17 @@ (* properties *) -fun make_notation {kind, name} = - Properties.print_eq (Markup.notationN, cartouche (implode_space (remove (op =) "" [kind, name]))); +fun block_annotation indent notation_markup notation_name = + let + val (elem, props) = notation_markup |> notation_name <> "" ? Markup.name notation_name; + val kind = Properties.get props Markup.kindN; + val name = Properties.get props Markup.nameN; + val s1 = if indent = 0 then [] else ["indent=" ^ Value.print_int indent]; + val s2 = + if elem = Markup.notationN then + [Properties.print_eq (elem, cartouche (implode_space (the_list kind @ the_list name)))] + else raise Fail ("Bad markup element for notatio: " ^ quote elem) + in cartouche (implode_space (s1 @ s2)) end; fun show_names names = commas_quote (map (fn (name, pos) => Markup.markup (Position.markup pos) name) names); @@ -157,19 +166,19 @@ (parse (b, pos2) handle Fail msg => error (msg ^ " for property " ^ quote name ^ Position.here_list [pos1, pos2]))); -fun parse_notation (s, pos) = +fun parse_notation ctxt (s, pos) = let val (kind, name) = (case Symbol.explode_words s of [] => ("", "") | a :: bs => (a, space_implode " " bs)); - in - if kind = "" orelse member (op =) Markup.notations kind then - Markup.notation {kind = kind, name = name} - else - error ("Bad notation kind " ^ quote kind ^ Position.here pos ^ - ", expected: " ^ commas_quote Markup.notations) - end; + val markup = + (case try (fn () => Markup_Kind.check_notation ctxt (kind, Position.none)) () of + SOME m => m + | NONE => + error ("Bad notation kind " ^ quote kind ^ Position.here pos ^ + ", expected: " ^ commas_quote (Markup_Kind.get_notation_kinds ctxt))); + in markup |> Markup.properties (Markup.name_proper name) end; in @@ -190,8 +199,8 @@ val get_bool = get_property false true (Value.parse_bool o #1); val get_nat = get_property 0 1 (Value.parse_nat o #1); -val get_notation_markup = - get_property NONE (SOME Markup.notation0) (SOME o parse_notation) Markup.notationN; +fun get_notation_markup ctxt = + get_property NONE (SOME Markup.notation0) (SOME o parse_notation ctxt) Markup.notationN; fun get_expression_markup ctxt = get_property NONE (SOME Markup.expression0) (SOME o Markup_Kind.check_expression ctxt) @@ -242,7 +251,7 @@ val props = read_properties ss; val more_markups = - the_list (get_notation_markup props) @ + the_list (get_notation_markup ctxt props) @ the_list (get_expression_markup ctxt props); val markup_name = get_string Markup.markupN props;