# HG changeset patch # User wenzelm # Date 1726839316 -7200 # Node ID 8ad5e6df050bf3f7c476aaa21ec4c16d50d18d7a # Parent 406a85a25189241992b97941f08acf478c28b641 block markup for specific notation, notably infix and binder; tuned; diff -r 406a85a25189 -r 8ad5e6df050b src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Fri Sep 20 14:28:13 2024 +0200 +++ b/src/Pure/PIDE/markup.ML Fri Sep 20 15:35:16 2024 +0200 @@ -67,6 +67,12 @@ val position_properties: string list val position_property: Properties.entry -> bool val def_name: string -> string + val notation_mixfixN: string + val notation_infixN: string + val notation_binderN: string + val notations: string list + val notationN: string val notation: {kind: string, name: string} -> T + val notation0: T val expressionN: string val expression: string -> T val expression0: T val citationN: string val citation: string -> T @@ -434,6 +440,19 @@ | NONE => make_def a); +(* notation: mixfix annotations *) + +val notation_mixfixN = "mixfix"; +val notation_infixN = "infix"; +val notation_binderN = "binder"; +val notations = [notation_mixfixN, notation_infixN, notation_binderN]; + +val notationN = "notation"; +fun notation {kind, name} = (notationN, kind_proper kind @ name_proper name); + +val notation0 = (notationN, []); + + (* expression *) val expressionN = "expression"; @@ -463,7 +482,7 @@ val unbreakableN = "unbreakable"; val indentN = "indent"; -val block_properties = [expressionN, markupN, consistentN, unbreakableN, indentN]; +val block_properties = [notationN, expressionN, markupN, consistentN, unbreakableN, indentN]; val widthN = "width"; diff -r 406a85a25189 -r 8ad5e6df050b src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Fri Sep 20 14:28:13 2024 +0200 +++ b/src/Pure/PIDE/markup.scala Fri Sep 20 15:35:16 2024 +0200 @@ -163,6 +163,18 @@ def def_name(a: String): String = def_names.getOrElse(a, a + "def_") + /* notation */ + + val NOTATION = "notation" + object Notation { + def unapply(markup: Markup): Option[(String, String)] = + markup match { + case Markup(NOTATION, props) => Some((Kind.get(props), Name.get(props))) + case _ => None + } + } + + /* expression */ val EXPRESSION = "expression" diff -r 406a85a25189 -r 8ad5e6df050b src/Pure/PIDE/rendering.scala --- a/src/Pure/PIDE/rendering.scala Fri Sep 20 14:28:13 2024 +0200 +++ b/src/Pure/PIDE/rendering.scala Fri Sep 20 15:35:16 2024 +0200 @@ -223,8 +223,8 @@ val text_color_elements = Markup.Elements(text_color.keySet) val tooltip_elements = - Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY, - Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING, + Markup.Elements(Markup.LANGUAGE, Markup.NOTATION, Markup.EXPRESSION, Markup.TIMING, + Markup.ENTITY, Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING, Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name) ++ Markup.Elements(tooltip_descriptions.keySet) @@ -663,6 +663,14 @@ case (info, Text.Info(r0, XML.Elem(Markup.Language(lang), _))) => Some(info + (r0, true, XML.Text("language: " + lang.description))) + case (info, Text.Info(r0, XML.Elem(Markup.Notation(kind, name), _))) => + val a = kind.nonEmpty + val b = name.nonEmpty + val description = + if (!a && !b) "notation" + else "notation: " + kind + if_proper(a && b, " ") + if_proper(b, quote(name)) + Some(info + (r0, true, XML.Text(description))) + case (info, Text.Info(r0, XML.Elem(Markup.Expression(kind), _))) => val description = if (kind.isEmpty) "expression" diff -r 406a85a25189 -r 8ad5e6df050b src/Pure/Syntax/mixfix.ML --- a/src/Pure/Syntax/mixfix.ML Fri Sep 20 14:28:13 2024 +0200 +++ b/src/Pure/Syntax/mixfix.ML Fri Sep 20 15:35:16 2024 +0200 @@ -151,6 +151,47 @@ else []; +(* infix notation *) + +val prefix_bg = Symbol_Pos.explode0 "'("; +val prefix_en = Symbol_Pos.explode0 "')"; + +val infix_bg = Symbol_Pos.explode0 "("; +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; + + +(* binder notation *) + +val binder_stamp = stamp (); +val binder_name = suffix "_binder"; + +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_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) = + [Type ("idts", []), ty2] ---> ty3 + | binder_typ c _ = error ("Bad type of binder: " ^ quote c); + + (* syn_ext_types *) val typeT = Type ("type", []); @@ -159,9 +200,10 @@ fun syn_ext_types ctxt type_decls = let fun mk_infix sy ty t p1 p2 p3 pos = - Syntax_Ext.Mfix - (Symbol_Pos.explode0 "(_ " @ Input.source_explode sy @ Symbol_Pos.explode0 "/ _)", - ty, t, [p1, p2], p3, pos); + let + val ss = Input.source_explode sy; + val syms = infix_block ctxt ss @ infix_arg1 @ ss @ infix_arg2; + in Syntax_Ext.Mfix (syms, ty, t, [p1, p2], p3, pos) end; fun mfix_of (t, ty, mx) = (case mx of @@ -190,37 +232,30 @@ (* syn_ext_consts *) -val binder_stamp = stamp (); -val binder_name = suffix "_binder"; - -fun mk_prefix sy = - let val sy' = Input.source_explode (Input.reset_pos sy); - in Symbol_Pos.explode0 "'(" @ sy' @ Symbol_Pos.explode0 "')" end - fun syn_ext_consts ctxt logical_types const_decls = let fun mk_infix sy ty c p1 p2 p3 pos = - [Syntax_Ext.Mfix (mk_prefix sy, ty, c, [], 1000, Position.none), - Syntax_Ext.Mfix - (Symbol_Pos.explode0 "(_ " @ Input.source_explode sy @ Symbol_Pos.explode0 "/ _)", - ty, c, [p1, p2], p3, pos)]; - - fun binder_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) = - [Type ("idts", []), ty2] ---> ty3 - | binder_typ c _ = error ("Bad type of binder: " ^ quote c); + let + val ss0 = Input.source_explode (Input.reset_pos sy); + val ss = Input.source_explode sy; + val syms = infix_block ctxt ss @ infix_arg1 @ ss @ infix_arg2; + in + [Syntax_Ext.Mfix (prefix_bg @ ss0 @ prefix_en, ty, c, [], 1000, Position.none), + Syntax_Ext.Mfix (syms, ty, c, [p1, p2], p3, pos)] + end; fun mfix_of (c, ty, mx) = (case mx of NoSyn => [] - | Mixfix (sy, ps, p, _) => - [Syntax_Ext.Mfix (Input.source_explode sy, ty, c, ps, p, pos_of mx)] + | Mixfix (sy, ps, p, _) => [Syntax_Ext.Mfix (Input.source_explode sy, ty, c, ps, p, pos_of mx)] | Infix (sy, p, _) => mk_infix sy ty c (p + 1) (p + 1) p (pos_of mx) | Infixl (sy, p, _) => mk_infix sy ty c p (p + 1) p (pos_of mx) | Infixr (sy, p, _) => mk_infix sy ty c (p + 1) p p (pos_of mx) | Binder (sy, p, q, _) => - [Syntax_Ext.Mfix - (Symbol_Pos.explode0 "(3" @ Input.source_explode sy @ Symbol_Pos.explode0 "_./ _)", - binder_typ c ty, (binder_name c), [0, p], q, pos_of mx)] + let + val ss = Input.source_explode sy; + val syms = binder_block ctxt ss @ ss @ binder_en; + in [Syntax_Ext.Mfix (syms, binder_typ c ty, binder_name c, [0, p], q, pos_of mx)] end | _ => error ("Bad mixfix declaration for " ^ quote c ^ Position.here (pos_of mx))); fun binder (c, _, Binder _) = SOME (binder_name c, c) diff -r 406a85a25189 -r 8ad5e6df050b src/Pure/Syntax/syntax_ext.ML --- a/src/Pure/Syntax/syntax_ext.ML Fri Sep 20 14:28:13 2024 +0200 +++ b/src/Pure/Syntax/syntax_ext.ML Fri Sep 20 15:35:16 2024 +0200 @@ -29,6 +29,8 @@ 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 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 val escape: string -> string @@ -121,6 +123,9 @@ (* properties *) +fun make_notation {kind, name} = + Properties.print_eq (Markup.notationN, cartouche (implode_space (remove (op =) "" [kind, name]))); + fun show_names names = commas_quote (map (fn (name, pos) => Markup.markup (Position.markup pos) name) names); @@ -152,6 +157,20 @@ (parse (b, pos2) handle Fail msg => error (msg ^ " for property " ^ quote name ^ Position.here_list [pos1, pos2]))); +fun parse_notation (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; + in fun read_properties ss = @@ -171,6 +190,9 @@ 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_expression_markup ctxt = get_property NONE (SOME Markup.expression0) (SOME o Markup_Expression.check ctxt) Markup.expressionN; @@ -219,7 +241,9 @@ let val props = read_properties ss; - val more_markups = the_list (get_expression_markup ctxt props); + val more_markups = + the_list (get_notation_markup props) @ + the_list (get_expression_markup ctxt props); val markup_name = get_string Markup.markupN props; val markup_props = props |> map_filter (fn (a, opt_b) => @@ -286,6 +310,9 @@ val read_mfix0 = read_mfix o Context_Position.set_visible false; +fun mfix_name ctxt = + read_mfix0 ctxt #> map_filter (fn (Delim s, _) => SOME s | _ => NONE) #> space_implode " "; + fun mfix_args ctxt ss = Integer.build (read_mfix0 ctxt ss |> fold (fn (xsymb, _) => is_argument xsymb ? Integer.add 1)); diff -r 406a85a25189 -r 8ad5e6df050b src/Tools/jEdit/src/jedit_rendering.scala --- a/src/Tools/jEdit/src/jedit_rendering.scala Fri Sep 20 14:28:13 2024 +0200 +++ b/src/Tools/jEdit/src/jedit_rendering.scala Fri Sep 20 15:35:16 2024 +0200 @@ -127,7 +127,7 @@ private val breakpoint_elements = Markup.Elements(Markup.ML_BREAKPOINT) private val highlight_elements = - Markup.Elements(Markup.EXPRESSION, Markup.LANGUAGE, Markup.ML_TYPING, + Markup.Elements(Markup.NOTATION, Markup.EXPRESSION, Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL, Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.FREE, Markup.SKOLEM, Markup.BOUND, Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_BREAKPOINT,