--- 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";
--- 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"
--- 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"
--- 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)
--- 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));
--- 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,