forked from Isabelle_DOF/Isabelle_DOF
Ongoing handling of ide interaction for string attributes
Ongoing handling of ide interaction of string type attribute value of instances as input source. The idea is when an attribute is a string type, then handle its value as an input source so that interaction with PIDE will be optimal: - if the attribute is not a string type then we parse it using Parse.term - if this is a string type, then we parse it with Parse.document_source and then we convert it to a string and try to parse it as a term. If the parsing fails, we handle the error and update the string by enclosing it with cartouches so that it can be understand as a hol string using frederic tuong hol string implementation (hol string declared with cartouche and not double simple quotes). Then we pass it to the code that generate the instance (cmd function). If this is not a well formed hol string we get an error.
This commit is contained in:
Nicolas Méric
parent
e78a114879
commit
a31098c98d
|
|
@ -19,9 +19,8 @@ text\<open>
|
|||
\end{frame}
|
||||
\<close>
|
||||
|
||||
|
||||
frame*[test_frame
|
||||
, frametitle = \<open>\<open>\<open>Example Slide\<^sub>t\<^sub>e\<^sub>s\<^sub>t\<close> with items @{thm "HOL.refl"}\<close>\<close>
|
||||
frame*[test_frame::frame
|
||||
, frametitle = \<open>\<open>Example Slide\<^sub>t\<^sub>e\<^sub>s\<^sub>t\<close> with items @{thm "HOL.refl"}\<close>
|
||||
, framesubtitle = "''Subtitle''"]
|
||||
\<open>This is an example!
|
||||
\<^item> The term \<^term>\<open>refl\<close> is...
|
||||
|
|
|
|||
|
|
@ -98,7 +98,29 @@ value*\<open>@{A \<open>xcv1\<close>}\<close>
|
|||
|
||||
text\<open>We can also get the value of an attribute of the instance:\<close>
|
||||
value*\<open>A.x @{A \<open>xcv1\<close>}\<close>
|
||||
find_consts name:"Conceptual.Isabelle_DOF_doc_class_A"
|
||||
find_theorems name:"Conceptual.Isabelle_DOF_doc_class_A"
|
||||
find_consts name:"xcv1"
|
||||
ML\<open>
|
||||
val t = \<^const>\<open>xcv1\<close>
|
||||
\<close>
|
||||
find_theorems name:"xcv1"
|
||||
ML\<open>
|
||||
val t = \<^term_>\<open>A.x @{A \<open>xcv1\<close>} = 2::int\<close>
|
||||
\<close>
|
||||
ML\<open>
|
||||
val t = Parse.const (Token.make_string0 "A.x @{A \<open>xcv1\<close>}" |> single)
|
||||
val tt = t |> fst |> YXML.content_of
|
||||
\<close>
|
||||
ML\<open>
|
||||
val ctxt = \<^context>
|
||||
\<close>
|
||||
ML\<open>
|
||||
val t = Parse.const (Token.make_string0 "A.x @{A \<open>xcv1\<close>}" |> single) |> fst
|
||||
val tt = YXML.parse_body t
|
||||
(*val tt = Term_XML.Decode.term (Proof_Context.consts_of ctxt) (YXML.parse_body t)*)
|
||||
|
||||
\<close>
|
||||
text\<open>If the attribute of the instance is not initialized, we get an undefined value,
|
||||
whose type is the type of the attribute:\<close>
|
||||
term*\<open>B.level @{C \<open>xcv2\<close>}\<close>
|
||||
|
|
|
|||
|
|
@ -850,7 +850,7 @@ fun block_antiquotation name scan =
|
|||
val _ = block_antiquotation \<^binding>\<open>block\<close> (block_modes -- Scan.lift Parse.document_source)
|
||||
|> Theory.setup
|
||||
|
||||
fun convert_meta_args ctxt (X, (((str,_),value) :: R)) =
|
||||
(*fun convert_meta_args ctxt (X, (((str,_),value) :: R)) =
|
||||
(case YXML.content_of str of
|
||||
"frametitle" => upd_frametitle (K(YXML.content_of value |> read_string))
|
||||
o convert_meta_args ctxt (X, R)
|
||||
|
|
@ -859,16 +859,146 @@ fun convert_meta_args ctxt (X, (((str,_),value) :: R)) =
|
|||
| "options" => upd_options (K(YXML.content_of value |> read_string))
|
||||
o convert_meta_args ctxt (X, R)
|
||||
| s => error("!undefined attribute:"^s))
|
||||
| convert_meta_args _ (_,[]) = I*)
|
||||
|
||||
fun convert_meta_args ctxt (X, (((str,_),value) :: R)) =
|
||||
(case YXML.content_of str of
|
||||
"frametitle" => upd_frametitle (K value)
|
||||
o convert_meta_args ctxt (X, R)
|
||||
| "framesubtitle" => upd_framesubtitle (K value)
|
||||
o convert_meta_args ctxt (X, R)
|
||||
| "options" => upd_options (K value)
|
||||
o convert_meta_args ctxt (X, R)
|
||||
| s => error("!undefined attribute:"^s))
|
||||
| convert_meta_args _ (_,[]) = I
|
||||
|
||||
type meta_args_t = (binding * (string * Position.T) option)
|
||||
* ((string * Position.T) * Input.source) list
|
||||
|
||||
type meta_args_t' = (binding * (string * Position.T) option)
|
||||
* ((string * Position.T) * string) list
|
||||
|
||||
val attribute =
|
||||
Parse.position Parse.const
|
||||
--| ODL_Meta_Args_Parser.improper
|
||||
-- Scan.optional (Parse.$$$ "=" --| ODL_Meta_Args_Parser.improper |-- Parse.document_source --| ODL_Meta_Args_Parser.improper) Input.empty
|
||||
: ((string * Position.T) * Input.source) parser;
|
||||
|
||||
val attributes =
|
||||
((Parse.$$$ "["
|
||||
-- ODL_Meta_Args_Parser.improper
|
||||
|-- (ODL_Meta_Args_Parser.reference --
|
||||
(Scan.optional(Parse.$$$ "," -- ODL_Meta_Args_Parser.improper |-- (Parse.enum "," (ODL_Meta_Args_Parser.improper |-- attribute)))) []))
|
||||
--| Parse.$$$ "]"
|
||||
--| ODL_Meta_Args_Parser.improper) : meta_args_t parser
|
||||
|
||||
val attribute' =
|
||||
Parse.position Parse.const
|
||||
--| ODL_Meta_Args_Parser.improper
|
||||
-- Scan.optional (Parse.$$$ "=" --| ODL_Meta_Args_Parser.improper |-- Parse.term --| ODL_Meta_Args_Parser.improper) "True"
|
||||
: ((string * Position.T) * string) parser;
|
||||
|
||||
val attributes' =
|
||||
((Parse.$$$ "["
|
||||
-- ODL_Meta_Args_Parser.improper
|
||||
|-- (ODL_Meta_Args_Parser.reference --
|
||||
(Scan.optional(Parse.$$$ "," -- ODL_Meta_Args_Parser.improper |-- (Parse.enum "," (ODL_Meta_Args_Parser.improper |-- attribute')))) []))
|
||||
--| Parse.$$$ "]"
|
||||
--| ODL_Meta_Args_Parser.improper) : meta_args_t' parser
|
||||
|
||||
fun document_command (name, pos) descr mark cmd sem_attrs transform_attr =
|
||||
Outer_Syntax.command (name, pos) descr
|
||||
(ODL_Meta_Args_Parser.attributes -- Parse.document_source >> (fn (meta_args, text) =>
|
||||
Toplevel.theory' (fn _ => cmd meta_args)
|
||||
(SOME (Toplevel.presentation_context #> Monitor_Command_Parser.document_output_reports name mark sem_attrs transform_attr meta_args text))));
|
||||
|
||||
fun onto_macro_cmd_output_reports output_cmd (meta_args, text) ctxt =
|
||||
let
|
||||
val _ = Context_Position.reports ctxt (Document_Output.document_reports text);
|
||||
in output_cmd (meta_args, text) ctxt end
|
||||
|
||||
fun dynamic_cartouche_parsing meta_args cmd thy =
|
||||
let
|
||||
val (((binding,cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) = meta_args
|
||||
val _ = writeln ("In dynamic_cartouche_parsing ((binding,cid_pos), doc_attrs): "
|
||||
^ \<^make_string> ((binding,cid_pos), doc_attrs))
|
||||
val (name_cid_typ, pos) = Value_Command.Docitem_Parser.check_classref {is_monitor = false} cid_pos thy
|
||||
val class_typ = name_cid_typ |> snd
|
||||
val fields = Record.get_recT_fields thy class_typ |> fst
|
||||
val _ = writeln ("In dynamic_cartouche_parsing fields: " ^ \<^make_string> fields)
|
||||
val fields' = fields |> map (apfst Long_Name.base_name)
|
||||
val _ = writeln ("In dynamic_cartouche_parsing fields': " ^ \<^make_string> fields')
|
||||
val doc_attrs' = doc_attrs
|
||||
|> map (fn ((name, pos), s)
|
||||
=> let val _ = writeln ("In dynamic_cartouche_parsing ((name,pos), s): "
|
||||
^ \<^make_string> ((name, pos), s))
|
||||
in if fields |> exists (fn (name', typ) => (equal (YXML.content_of name) (Long_Name.base_name name')
|
||||
andalso equal \<^typ>\<open>char list\<close> typ))
|
||||
then let val v = Syntax.parse_term (Proof_Context.init_global thy) s handle ERROR _ => \<^term>\<open>''Undefined_String''\<close>
|
||||
in let val _ = writeln ("In dynamic_cartouche_parsing v: " ^ \<^make_string> v)
|
||||
in if v = \<^term>\<open>''Undefined_String''\<close>
|
||||
then ((name, pos), cartouche s)
|
||||
else ((name, pos), s)
|
||||
end
|
||||
end
|
||||
else ((name, pos), s)
|
||||
end)
|
||||
val _ = writeln ("In dynamic_cartouche_parsing doc_attrs': " ^ \<^make_string> (doc_attrs' |> map (apfst (apfst (YXML.content_of)))))
|
||||
in cmd ((binding,cid_pos), doc_attrs') thy end
|
||||
|
||||
fun choose_parser meta_args cid =
|
||||
let
|
||||
val (((binding,cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) = meta_args
|
||||
val _ = writeln ("In choose_parser ((binding,cid_pos), doc_attrs): "
|
||||
^ \<^make_string> ((binding,cid_pos), doc_attrs))
|
||||
val thy = Context.the_global_context ()
|
||||
val (name_cid_typ, pos) = Value_Command.Docitem_Parser.check_classref {is_monitor = false} (SOME (cid, Position.none)) thy
|
||||
val class_typ = name_cid_typ |> snd
|
||||
val fields = Record.get_recT_fields thy class_typ |> fst
|
||||
val _ = writeln ("In choose_parser fields: " ^ \<^make_string> fields)
|
||||
val fields' = fields |> map (apfst Long_Name.base_name)
|
||||
val _ = writeln ("In choose_parser fields': " ^ \<^make_string> fields')
|
||||
val doc_attrs' = doc_attrs
|
||||
|> map (fn ((name, pos), s)
|
||||
=> let val _ = writeln ("In choose_parser ((name,pos), s): "
|
||||
^ \<^make_string> ((name, pos), s))
|
||||
in if fields |> exists (fn (name', typ) => (equal (YXML.content_of name) (Long_Name.base_name name')
|
||||
andalso equal \<^typ>\<open>char list\<close> typ))
|
||||
then let val v = Syntax.parse_term (Proof_Context.init_global thy) s handle ERROR _ => \<^term>\<open>''Undefined_String''\<close>
|
||||
in let val _ = writeln ("In choose_parser v: " ^ \<^make_string> v)
|
||||
in if v = \<^term>\<open>''Undefined_String''\<close>
|
||||
then ((name, pos), cartouche s)
|
||||
else ((name, pos), s)
|
||||
end
|
||||
end
|
||||
else ((name, pos), s)
|
||||
end)
|
||||
val _ = writeln ("In choose_parser doc_attrs': " ^ \<^make_string> (doc_attrs' |> map (apfst (apfst (YXML.content_of)))))
|
||||
in () end
|
||||
|
||||
fun onto_macro_cmd_command (name, pos) descr cmd output_cmd cid =
|
||||
Outer_Syntax.command (name, pos) descr
|
||||
(attributes -- Parse.document_source >>
|
||||
(fn (meta_args, text) =>
|
||||
Toplevel.theory' (meta_args |> apsnd (map (apsnd (Input.string_of)))
|
||||
|> (fn meta_args => dynamic_cartouche_parsing meta_args cmd)
|
||||
|> K)
|
||||
(SOME (Toplevel.presentation_context
|
||||
#> onto_macro_cmd_output_reports output_cmd (meta_args, text)
|
||||
))))
|
||||
|
||||
fun frame_command (name, pos) descr cid =
|
||||
let fun set_default_class NONE = SOME(cid,pos)
|
||||
|set_default_class (SOME X) = SOME X
|
||||
fun create_instance (((binding,cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) =
|
||||
let val _ = writeln ("In frame_command in create_instance ((binding,cid_pos), doc_attrs): "
|
||||
^ \<^make_string> ((binding,cid_pos), doc_attrs))
|
||||
in
|
||||
Value_Command.Docitem_Parser.create_and_check_docitem
|
||||
{is_monitor = false}
|
||||
{is_inline = true}
|
||||
{define = true} binding (set_default_class cid_pos) doc_attrs
|
||||
end
|
||||
fun titles_src ctxt frametitle framesubtitle src =
|
||||
Latex.string "{"
|
||||
@ Document_Output.output_document ctxt {markdown = false} frametitle
|
||||
|
|
@ -890,11 +1020,14 @@ fun frame_command (name, pos) descr cid =
|
|||
end
|
||||
end
|
||||
fun parse_and_tex (margs, src) ctxt =
|
||||
let val _ = writeln ("In frame_command in parse_and_tex margs: " ^ \<^make_string> margs)
|
||||
in
|
||||
convert_meta_args ctxt margs
|
||||
|> generate_src_ltx_ctxt ctxt src
|
||||
|> Latex.environment ("frame")
|
||||
|> Latex.environment ("isamarkuptext")
|
||||
in Monitor_Command_Parser.onto_macro_cmd_command (name, pos) descr create_instance parse_and_tex
|
||||
end
|
||||
in onto_macro_cmd_command (name, pos) descr create_instance parse_and_tex cid
|
||||
end
|
||||
|
||||
val _ = frame_command \<^command_keyword>\<open>frame*\<close> "frame environment" "Isa_COL.frame" ;
|
||||
|
|
|
|||
|
|
@ -1926,6 +1926,7 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} bi
|
|||
|> (fn thy => if default_cid then thy
|
||||
else if Config.get_global thy DOF_core.invariants_checking
|
||||
then check_invariants thy binding else thy))
|
||||
|> Sign.add_consts [(binding, \<^typ>\<open>string\<close>, Mixfix.NoSyn)]
|
||||
end
|
||||
|
||||
end (* structure Docitem_Parser *)
|
||||
|
|
@ -3126,7 +3127,7 @@ fun add_doc_class_cmd overloaded (raw_params, binding)
|
|||
val invariants' = invariants |> map (apfst (Binding.qualify false name
|
||||
#> Binding.suffix_name invariant_suffixN))
|
||||
in thy (* adding const symbol representing doc-class for Monitor-RegExps.*)
|
||||
|> Named_Target.theory_map (def_cmd args)
|
||||
|> Named_Target.theory_map (def_cmd args)
|
||||
|> (case parent' of
|
||||
NONE => add (DOF_core.tag_attr::record_fields) invariants' {virtual=false}
|
||||
| SOME _ => if (not o null) record_fields
|
||||
|
|
|
|||
Loading…
Reference in New Issue