From 8ade5f96791054d02ba92e5e40a4d087a80b9155 Mon Sep 17 00:00:00 2001 From: Rafal Kolanski Date: Tue, 20 Aug 2024 12:54:58 +1000 Subject: [PATCH] lib: Requalify: enable ctrl+click jumps for arch_requalify This uses a complex workaround to unify the parse location of the original name encoded in YXML with the name the user is actually aiming for. While intuitively one could think to use the position of the name we parsed, there appears to be no way to pass that location to read_const/read_type_name, as those expect to be fed the result of Parse.const and Parse.typ respectively. Signed-off-by: Rafal Kolanski --- lib/Requalify.thy | 38 +++++++++++++++++++++++++++++--------- 1 file changed, 29 insertions(+), 9 deletions(-) diff --git a/lib/Requalify.thy b/lib/Requalify.thy index 84dffdc8b5..ff36e957cf 100644 --- a/lib/Requalify.thy +++ b/lib/Requalify.thy @@ -8,7 +8,6 @@ (* Requalify constants, types and facts into the current naming. Includes command variants that support implicitly using the L4V_ARCH environment variable. - *) text \See theory @{text "test/Requalify_Test.thy"} for commented examples and usage scenarios.\ @@ -141,6 +140,29 @@ val get_fact_nm = (fst oo global_fact) global_fact are accessible in the current context. *) fun check_fact lthy (_, (nm, pos)) = Proof_Context.get_fact lthy (Facts.Named ((nm,pos), NONE)) +(* replace text in all Text nodes in YXML-encoded string entry with new_text *) +fun replace_yxml_text new_text = +let + fun tree_text (XML.Text _) = XML.Text new_text + | tree_text (XML.Elem (node, trees)) = (XML.Elem (node, map tree_text trees)) +in + YXML.string_of o tree_text o YXML.parse +end + +(* These versions, prior to resolving the const/type name, override that name in the parsed + YXML-encoded string entry with a name that will actually resolve to something, while preserving + other parse data such as parsed document location. + This updates the document markup at the original parse location of entry with a reference to the + const/type named by "name", allowing the user to ctrl+click to jump to the const/type definition. + + For example, if the user requested "arch_requalify_consts (A) some_const", then they are + targeting something like "ARM_H.some_const", and expect to be able to jump to its definition. + + This isn't necessary for facts, as those use parsed position of "name" directly via + Proof_Context.get_fact, which appears not available for read_const/read_type_name. *) +fun arch_const_nm lthy entry name = get_const_nm lthy (replace_yxml_text name entry) +fun arch_type_nm lthy entry name = get_type_nm lthy (replace_yxml_text name entry) + in val _ = @@ -168,22 +190,20 @@ val _ = "arch_requalify_consts (H) const" becomes "requalify_consts ARM_H.const" This allows them to be used in a architecture-generic theory. - For consts and types, we don't perform extra checking on the results of Parse.const and Parse.typ - because their "strings" contain embedded syntax, which means prepending a normal string to them - causes malformed syntax and YXML exceptions. It shouldn't matter, we are looking up the name and - checking it's a constant/type anyway. *) + For consts and types, we need to perform text replacement in the YXML entry to combine the parse + location with the right const/type name (see arch_const_nm and arch_type_nm). *) val _ = Outer_Syntax.command @{command_keyword arch_requalify_consts} "alias const with current naming, but prepend \"($L4V_ARCH)_[A|H].\" using env. variable" - (gen_requalify get_const_nm Parse.const (fn _ => fn (_, _) => ()) const_alias - true) + (gen_requalify get_const_nm Parse.const (fn lthy => fn (e, (nm, _)) => arch_const_nm lthy e nm) + const_alias true) val _ = Outer_Syntax.command @{command_keyword arch_requalify_types} "alias type with current naming, but prepend \"($L4V_ARCH)_[A|H].\" using env. variable" - (gen_requalify get_type_nm Parse.typ (fn _ => fn (_, _) => ()) type_alias - true) + (gen_requalify get_type_nm Parse.typ (fn lthy => fn (e, (nm, _)) => arch_type_nm lthy e nm) + type_alias true) val _ = Outer_Syntax.command @{command_keyword arch_requalify_facts}