# HG changeset patch # User wenzelm # Date 1733611818 -3600 # Node ID b57996a0688c255cd4e72d0367fbdbfccf24250a # Parent 8dc9453889caf8c45768930bfd924b3a2554574d clarified term positions and markup: syntax = true means this is via concrete syntax; clarified text color rendering; diff -r 8dc9453889ca -r b57996a0688c src/HOL/ex/Cartouche_Examples.thy --- a/src/HOL/ex/Cartouche_Examples.thy Sat Dec 07 23:08:51 2024 +0100 +++ b/src/HOL/ex/Cartouche_Examples.thy Sat Dec 07 23:50:18 2024 +0100 @@ -71,7 +71,7 @@ (case args of [(c as Const (\<^syntax_const>\_constrain\, _)) $ Free (s, _) $ p] => (case Term_Position.decode_position1 p of - SOME pos => c $ mk_string (content (s, pos)) $ p + SOME {pos, ...} => c $ mk_string (content (s, pos)) $ p | NONE => err ()) | _ => err ()) end; diff -r 8dc9453889ca -r b57996a0688c src/Pure/Build/browser_info.scala --- a/src/Pure/Build/browser_info.scala Sat Dec 07 23:08:51 2024 +0100 +++ b/src/Pure/Build/browser_info.scala Sat Dec 07 23:50:18 2024 +0100 @@ -522,7 +522,7 @@ case _ => body1 } - Rendering.foreground.get(name) orElse Rendering.get_text_color(name) match { + Rendering.foreground.get(name) orElse Rendering.get_text_color(markup) match { case Some(c) => (html_class(c.toString, html), offset) case None => (html_class(name, html), offset) } diff -r 8dc9453889ca -r b57996a0688c src/Pure/General/position.ML --- a/src/Pure/General/position.ML Sat Dec 07 23:08:51 2024 +0100 +++ b/src/Pure/General/position.ML Sat Dec 07 23:50:18 2024 +0100 @@ -54,8 +54,6 @@ type report_text = report * string val reports_text: report_text list -> unit val reports: report list -> unit - val store_reports: report_text list Unsynchronized.ref -> - T list -> ('a -> Markup.T list) -> 'a -> unit val append_reports: report_text list Unsynchronized.ref -> report list -> unit val here_strs: T -> string * string val here: T -> string @@ -271,11 +269,6 @@ val reports = map (rpair "") #> reports_text; -fun store_reports _ [] _ _ = () - | store_reports (r: report_text list Unsynchronized.ref) ps markup x = - let val ms = markup x - in Unsynchronized.change r (fold (fn p => fold (fn m => cons ((p, m), "")) ms) ps) end; - fun append_reports (r: report_text list Unsynchronized.ref) reports = Unsynchronized.change r (append (map (rpair "") reports)); diff -r 8dc9453889ca -r b57996a0688c src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Sat Dec 07 23:08:51 2024 +0100 +++ b/src/Pure/Isar/proof_context.ML Sat Dec 07 23:50:18 2024 +0100 @@ -790,7 +790,7 @@ Vartab.insert (op =) (xi, Type.minimize_sort tsig S) env handle Vartab.DUP _ => error ("Inconsistent sort constraints for type variable " ^ - quote (Term.string_of_vname' xi) ^ Position.here_list ps) + quote (Term.string_of_vname' xi) ^ Position.here_list (map #pos ps)) end; val env = @@ -821,7 +821,7 @@ fun get_sort_reports xi raw_S = let - val ps = #1 (Term_Position.decode_positionS raw_S); + val ps = map #pos (#1 (Term_Position.decode_positionS raw_S)); val S = get_sort xi raw_S handle ERROR msg => error (msg ^ Position.here_list ps); in fold (add_report S) ps end; diff -r 8dc9453889ca -r b57996a0688c src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Sat Dec 07 23:08:51 2024 +0100 +++ b/src/Pure/Isar/specification.ML Sat Dec 07 23:50:18 2024 +0100 @@ -100,7 +100,7 @@ | get _ (t $ u) = get [] t @ get [] u | get _ (Abs (_, _, t)) = get [] t | get _ _ = []; - in get [] end; + in map #pos o get [] end; local diff -r 8dc9453889ca -r b57996a0688c src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Sat Dec 07 23:08:51 2024 +0100 +++ b/src/Pure/PIDE/markup.ML Sat Dec 07 23:50:18 2024 +0100 @@ -196,6 +196,8 @@ val comment1N: string val comment1: T val comment2N: string val comment2: T val comment3N: string val comment3: T + val syntaxN: string val syntax_properties: bool -> T -> T + val has_syntax: Properties.T -> bool val elapsedN: string val cpuN: string val gcN: string @@ -675,6 +677,19 @@ val (comment3N, comment3) = markup_elem "comment3"; +(* concrete syntax (notably mixfix notation) *) + +val syntaxN = "syntax"; + +val syntax_elements = [improperN, freeN, skolemN]; + +fun syntax_properties syntax (m as (elem, props): T) = + if syntax andalso member (op =) syntax_elements elem + then (elem, Properties.put (syntaxN, "true") props) else m; + +fun has_syntax props = Properties.get_bool props syntaxN; + + (* timing *) val elapsedN = "elapsed"; diff -r 8dc9453889ca -r b57996a0688c src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Sat Dec 07 23:08:51 2024 +0100 +++ b/src/Pure/PIDE/markup.scala Sat Dec 07 23:50:18 2024 +0100 @@ -479,6 +479,13 @@ val COMMENT3 = "comment3" + /* concrete syntax (notably mixfix notation) */ + + val Syntax = new Properties.Boolean("syntax") + + def has_syntax(props: Properties.T): Boolean = Syntax.get(props) + + /* timing */ val Elapsed = new Properties.Double("elapsed") diff -r 8dc9453889ca -r b57996a0688c src/Pure/PIDE/rendering.scala --- a/src/Pure/PIDE/rendering.scala Sat Dec 07 23:08:51 2024 +0100 +++ b/src/Pure/PIDE/rendering.scala Sat Dec 07 23:50:18 2024 +0100 @@ -105,14 +105,20 @@ /* text color */ - def get_text_color(name: String): Option[Color.Value] = text_colors.get(name) + def get_text_color(markup: Markup): Option[Color.Value] = + if (Markup.has_syntax(markup.properties)) text_color2.get(markup.name) + else text_color1.get(markup.name) orElse text_color2.get(markup.name) - private val text_colors = Map( + private val text_color1 = Map( + Markup.IMPROPER -> Color.improper, + Markup.FREE -> Color.free, + Markup.SKOLEM -> Color.skolem) + + private val text_color2 = Map( Markup.KEYWORD1 -> Color.keyword1, Markup.KEYWORD2 -> Color.keyword2, Markup.KEYWORD3 -> Color.keyword3, Markup.QUASI_KEYWORD -> Color.quasi_keyword, - Markup.IMPROPER -> Color.improper, Markup.OPERATOR -> Color.operator, Markup.STRING -> Color.main, Markup.ALT_STRING -> Color.main, @@ -121,8 +127,6 @@ Markup.DELIMITER -> Color.main, Markup.TFREE -> Color.tfree, Markup.TVAR -> Color.tvar, - Markup.FREE -> Color.free, - Markup.SKOLEM -> Color.skolem, Markup.BOUND -> Color.bound, Markup.VAR -> Color.`var`, Markup.INNER_STRING -> Color.inner_quoted, @@ -222,7 +226,7 @@ val foreground_elements = Markup.Elements(foreground.keySet) - val text_color_elements = Markup.Elements(text_colors.keySet) + val text_color_elements = Markup.Elements(text_color1.keySet ++ text_color2.keySet) val structure_elements = Markup.Elements(Markup.NOTATION, Markup.EXPRESSION, Markup.LANGUAGE, Markup.ML_TYPING, diff -r 8dc9453889ca -r b57996a0688c src/Pure/Syntax/ast.ML --- a/src/Pure/Syntax/ast.ML Sat Dec 07 23:08:51 2024 +0100 +++ b/src/Pure/Syntax/ast.ML Sat Dec 07 23:50:18 2024 +0100 @@ -89,7 +89,7 @@ fun pretty_var x = (case Term_Position.decode x of [] => Pretty.str x - | ps => Term_Position.pretty ps); + | ps => Term_Position.pretty (map #pos ps)); fun pretty_ast (Constant a) = Pretty.quote (Pretty.str a) | pretty_ast (Variable x) = pretty_var x diff -r 8dc9453889ca -r b57996a0688c src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Sat Dec 07 23:08:51 2024 +0100 +++ b/src/Pure/Syntax/syntax_phases.ML Sat Dec 07 23:50:18 2024 +0100 @@ -61,8 +61,9 @@ fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var]; -fun markup_bound def ps (name, id) = - Markup.bound :: map (fn pos => Position.make_entity_markup def id Markup.boundN (name, pos)) ps; +fun markup_bound def (ps: Term_Position.T list) (name, id) = + Markup.bound :: + map (fn {pos, ...} => Position.make_entity_markup def id Markup.boundN (name, pos)) ps; fun markup_entity ctxt c = Syntax.get_consts (Proof_Context.syntax_of ctxt) c @@ -158,7 +159,7 @@ fun parsetree_to_ast ctxt trf parsetree = let val reports = Unsynchronized.ref ([]: Position.report_text list); - fun report pos = Position.store_reports reports [pos]; + fun report pos = Term_Position.store_reports reports [pos]; val append_reports = Position.append_reports reports; fun report_pos tok = @@ -168,8 +169,11 @@ val markup_cache = Symtab.apply_unsynchronized_cache (markup_entity ctxt); val ast_of_pos = Ast.Variable o Term_Position.encode; - val ast_of_position = ast_of_pos o single o report_pos; - fun ast_of_position' a = Ast.constrain (Ast.Constant a) o ast_of_position; + val ast_of_position = Ast.Variable o Term_Position.encode_no_syntax o single o report_pos; + + val syntax_ast_of_pos = Ast.Variable o Term_Position.encode_syntax; + val syntax_ast_of_position = syntax_ast_of_pos o single o report_pos; + fun syntax_ast_of_position' a = Ast.constrain (Ast.Constant a) o syntax_ast_of_position; fun asts_of_token tok = if Lexicon.valued_token tok @@ -201,21 +205,21 @@ val _ = append_reports rs; in [Ast.Constant (Lexicon.mark_type c)] end | asts_of (Parser.Node ({const = "_DDDOT", ...}, [Parser.Tip tok])) = - [Ast.constrain (Ast.Variable Auto_Bind.dddot_vname) (ast_of_position tok)] + [Ast.constrain (Ast.Variable Auto_Bind.dddot_vname) (syntax_ast_of_position tok)] | asts_of (Parser.Node ({const = "_position", ...}, [Parser.Tip tok])) = asts_of_position "_constrain" tok | asts_of (Parser.Node ({const = "_position_sort", ...}, [Parser.Tip tok])) = asts_of_position "_ofsort" tok | asts_of (Parser.Node ({const = a as "\<^const>Pure.dummy_pattern", ...}, [Parser.Tip tok])) = - [ast_of_position' a tok] + [syntax_ast_of_position' a tok] | asts_of (Parser.Node ({const = a as "_idtdummy", ...}, [Parser.Tip tok])) = - [ast_of_position' a tok] + [syntax_ast_of_position' a tok] | asts_of (Parser.Node ({const = "_idtypdummy", ...}, pts as [Parser.Tip tok, _, _])) = let val args = maps asts_of pts - in [Ast.Appl (Ast.Constant "_constrain" :: ast_of_position' "_idtdummy" tok :: args)] end + in [Ast.Appl (Ast.Constant "_constrain" :: syntax_ast_of_position' "_idtdummy" tok :: args)] end | asts_of (Parser.Node ({const = a, ...}, pts)) = let - val ps = maps parsetree_literals pts; + val ps = map Term_Position.syntax (maps parsetree_literals pts); val args = maps asts_of pts; fun head () = if not (null ps) andalso (Lexicon.is_fixed a orelse Lexicon.is_const a) @@ -272,7 +276,7 @@ | decode (reports0, Exn.Res tm) = let val reports = Unsynchronized.ref reports0; - fun report ps = Position.store_reports reports ps; + fun report ps = Term_Position.store_reports reports ps; val append_reports = Position.append_reports reports; fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) = @@ -299,13 +303,13 @@ let val c = #1 (decode_const ctxt (a, [])) in report ps markup_const_cache c; Const (c, T) end)) | decode ps _ _ (Free (a, T)) = - ((Name.reject_internal (a, ps) handle ERROR msg => - error (msg ^ Proof_Context.consts_completion_message ctxt (a, ps))); + ((Name.reject_internal (a, map #pos ps) handle ERROR msg => + error (msg ^ Proof_Context.consts_completion_message ctxt (a, map #pos ps))); (case Proof_Context.lookup_free ctxt a of SOME x => (report ps markup_free_cache x; Free (x, T)) | NONE => let - val (c, rs) = decode_const ctxt (a, ps); + val (c, rs) = decode_const ctxt (a, map #pos ps); val _ = append_reports rs; in Const (c, T) end)) | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T)) @@ -462,7 +466,7 @@ val syn = Proof_Context.syntax_of ctxt; val reports = Unsynchronized.ref ([]: Position.report_text list); - fun report ps = Position.store_reports reports ps; + fun report ps = Term_Position.store_reports reports ps; val markup_cache = Symtab.apply_unsynchronized_cache (markup_entity ctxt); @@ -765,11 +769,12 @@ val pretty_free_cache = Symtab.apply_unsynchronized_cache (pretty_free ctxt); val pretty_var_cache = Symtab.apply_unsynchronized_cache pretty_var; - val markup_syntax_cache = Symtab.apply_unsynchronized_cache (markup_entity ctxt); + val markup_syntax_cache = + Symtab.apply_unsynchronized_cache (markup_entity ctxt #> map (Markup.syntax_properties true)); val pretty_entity_cache = Symtab.apply_unsynchronized_cache (fn a => - Pretty.marks_str (markup_syntax_cache a, extern ctxt a)); + Pretty.marks_str (markup_entity ctxt a, extern ctxt a)); val cache1 = Unsynchronized.ref (Ast.Table.empty: Markup.output Pretty.block Ast.Table.table); val cache2 = Unsynchronized.ref (Ast.Table.empty: Markup.output Pretty.block Ast.Table.table); @@ -872,7 +877,7 @@ (case asts of [Ast.Appl [Ast.Constant "_constrain", Ast.Variable c, T as Ast.Variable p]] => let - val (c', _) = decode_const ctxt (c, Term_Position.decode p); + val (c', _) = decode_const ctxt (c, map #pos (Term_Position.decode p)); val d = if intern then Lexicon.mark_const c' else c; in Ast.constrain (Ast.Constant d) T end | _ => raise Ast.AST ("const_ast_tr", asts)); @@ -995,7 +1000,7 @@ |> apply_term_check ctxt |> chop (length ts); val typing_report = - fold2 (fn (pos, _) => fn ty => + fold2 (fn ({pos, ...}, _) => fn ty => if Position.is_reported pos then cons (Position.reported_text pos Markup.typing (Syntax.string_of_typ ctxt (Logic.dest_type ty))) diff -r 8dc9453889ca -r b57996a0688c src/Pure/Syntax/term_position.ML --- a/src/Pure/Syntax/term_position.ML Sat Dec 07 23:08:51 2024 +0100 +++ b/src/Pure/Syntax/term_position.ML Sat Dec 07 23:50:18 2024 +0100 @@ -6,16 +6,23 @@ signature TERM_POSITION = sig + type T = {syntax: bool, pos: Position.T} + val syntax: Position.T -> T + val no_syntax: Position.T -> T + val store_reports: Position.report_text list Unsynchronized.ref -> + T list -> ('a -> Markup.T list) -> 'a -> unit val pretty: Position.T list -> Pretty.T - val encode: Position.T list -> string + val encode: T list -> string + val encode_syntax: Position.T list -> string + val encode_no_syntax: Position.T list -> string val detect: string -> bool - val decode: string -> Position.T list + val decode: string -> T list val detect_position: term -> bool - val decode_position: term -> (Position.T list * typ) option - val decode_position1: term -> Position.T option + val decode_position: term -> (T list * typ) option + val decode_position1: term -> T option val detect_positionT: typ -> bool - val decode_positionT: typ -> Position.T list - val decode_positionS: sort -> Position.T list * sort + val decode_positionT: typ -> T list + val decode_positionS: sort -> T list * sort val markers: string list val strip_positions: term -> term end; @@ -23,6 +30,22 @@ structure Term_Position: TERM_POSITION = struct +(* type T *) + +type T = {syntax: bool, pos: Position.T}; + +fun syntax pos : T = {syntax = true, pos = pos}; +fun no_syntax pos : T = {syntax = false, pos = pos}; + +fun store_reports _ [] _ _ = () + | store_reports (r: Position.report_text list Unsynchronized.ref) ps markup x = + let + val ms = markup x; + fun store {syntax, pos} = + fold (fn m => cons ((pos, Markup.syntax_properties syntax m), "")) ms; + in Unsynchronized.change r (fold store ps) end; + + (* markup *) val position_dummy = ""; @@ -30,24 +53,28 @@ fun pretty ps = Pretty.marks_str (map Position.markup ps, position_dummy); -fun encode_pos pos = XML.Elem (Position.markup pos, [position_text]); +fun encode_pos {syntax, pos} = + XML.Elem (Position.markup pos |> Markup.syntax_properties syntax, [position_text]); fun decode_pos (XML.Elem ((name, props), [arg])) = if name = Markup.positionN andalso arg = position_text - then SOME (Position.of_properties props) + then SOME {syntax = Markup.has_syntax props, pos = Position.of_properties props} else NONE | decode_pos _ = NONE; (* encode *) -val encode_none = YXML.string_of (encode_pos Position.none); +val encode_none = YXML.string_of (encode_pos (no_syntax Position.none)); fun encode ps = - (case filter Position.is_reported ps of + (case filter (Position.is_reported o #pos) ps of [] => encode_none | ps' => YXML.string_of_body (map encode_pos ps')); +val encode_syntax = encode o map syntax; +val encode_no_syntax = encode o map no_syntax; + val encode_prefix = YXML.XY ^ Markup.positionN; @@ -56,7 +83,7 @@ val detect = String.isPrefix encode_prefix; fun decode str = - if str = encode_none then [Position.none] + if str = encode_none then [no_syntax Position.none] else if detect str then let val xml = YXML.parse_body str handle Fail msg => error msg; diff -r 8dc9453889ca -r b57996a0688c src/Pure/type_infer_context.ML --- a/src/Pure/type_infer_context.ML Sat Dec 07 23:08:51 2024 +0100 +++ b/src/Pure/type_infer_context.ML Sat Dec 07 23:50:18 2024 +0100 @@ -8,7 +8,7 @@ sig val const_sorts: bool Config.T val const_type: Proof.context -> string -> typ option - val prepare_positions: Proof.context -> term list -> term list * (Position.T * typ) list + val prepare_positions: Proof.context -> term list -> term list * (Term_Position.T * typ) list val prepare: Proof.context -> term list -> int * term list val infer_types: Proof.context -> term list -> term list val infer_types_finished: Proof.context -> term list -> term list diff -r 8dc9453889ca -r b57996a0688c src/Tools/VSCode/src/pretty_text_panel.scala --- a/src/Tools/VSCode/src/pretty_text_panel.scala Sat Dec 07 23:08:51 2024 +0100 +++ b/src/Tools/VSCode/src/pretty_text_panel.scala Sat Dec 07 23:50:18 2024 +0100 @@ -75,13 +75,13 @@ val document = Line.Document(text) val decorations = - tree.cumulate[Option[String]](Text.Range.full, None, Rendering.text_color_elements, - { case (_, m) => Some(Some(m.info.name)) } + tree.cumulate[Option[Markup]](Text.Range.full, None, Rendering.text_color_elements, + { case (_, m) => Some(Some(m.info.markup)) } ).flatMap(info => info.info match { - case Some(name) => + case Some(markup) => val range = document.range(info.range) - Some((range, "text_" + Rendering.get_text_color(name).get.toString)) + Some((range, "text_" + Rendering.get_text_color(markup).get.toString)) case None => None } ).groupMap(_._2)(e => LSP.Decoration_Options(e._1, Nil)).toList diff -r 8dc9453889ca -r b57996a0688c src/Tools/VSCode/src/vscode_rendering.scala --- a/src/Tools/VSCode/src/vscode_rendering.scala Sat Dec 07 23:08:51 2024 +0100 +++ b/src/Tools/VSCode/src/vscode_rendering.scala Sat Dec 07 23:50:18 2024 +0100 @@ -167,7 +167,7 @@ def text_color(range: Text.Range): List[Text.Info[Rendering.Color.Value]] = { snapshot.select(range, Rendering.text_color_elements, _ => { - case Text.Info(_, elem) => Rendering.get_text_color(elem.name) + case Text.Info(_, elem) => Rendering.get_text_color(elem.markup) }) } diff -r 8dc9453889ca -r b57996a0688c src/Tools/jEdit/src/jedit_rendering.scala --- a/src/Tools/jEdit/src/jedit_rendering.scala Sat Dec 07 23:08:51 2024 +0100 +++ b/src/Tools/jEdit/src/jedit_rendering.scala Sat Dec 07 23:50:18 2024 +0100 @@ -375,7 +375,7 @@ else snapshot.cumulate(range, current_color, Rendering.text_color_elements, _ => { - case (_, Text.Info(_, elem)) => Rendering.get_text_color(elem.name).map(color) + case (_, Text.Info(_, elem)) => Rendering.get_text_color(elem.markup).map(color) }) }