forked from Isabelle_DOF/Isabelle_DOF
boxed sml preserves now $.
This commit is contained in:
parent
ebce149d6a
commit
6cafcce536
|
@ -42,7 +42,7 @@ define_macro* nolinkurl \<rightleftharpoons> \<open>\nolinkurl{\<close> _ \<open
|
|||
define_macro* center \<rightleftharpoons> \<open>\center{\<close> _ \<open>}\<close>
|
||||
define_macro* ltxinline \<rightleftharpoons> \<open>\inlineltx|\<close> _ \<open>|\<close>
|
||||
|
||||
|
||||
ML\<open>curry (op ^) "[mathescape=false]" \<close>
|
||||
ML\<open>
|
||||
|
||||
fun boxed_text_antiquotation name (* redefined in these more abstract terms *) =
|
||||
|
@ -61,6 +61,7 @@ fun boxed_theory_text_antiquotation name (* redefined in these more abstract ter
|
|||
fun boxed_sml_text_antiquotation name =
|
||||
DOF_lib.gen_text_antiquotation name (K(K()))
|
||||
(fn ctxt => Input.source_content
|
||||
#> apfst (curry (op ^) "[mathescape=false]")
|
||||
#> Latex.text
|
||||
#> DOF_lib.enclose_env true ctxt "sml")
|
||||
(* the simplest conversion possible *)
|
||||
|
|
|
@ -22,10 +22,10 @@ chapter*[isadof_developers::text_section]\<open>Extending \<^isadof>\<close>
|
|||
text\<open>
|
||||
In this chapter, we describe the basic implementation aspects of \<^isadof>, which is based on
|
||||
the following design-decisions:
|
||||
\<^item> the entire \<^isadof> is a ``pure add-on,'' \<^ie>, we deliberately resign the possibility to
|
||||
\<^item> the entire \<^isadof> is a ``pure add-on,'' \<^ie>, we deliberately resign to the possibility to
|
||||
modify Isabelle itself,
|
||||
\<^item> we made a small exception to this rule: the \<^isadof> package modifies in its installation
|
||||
about 10 lines in the \LaTeX-generator (\path{src/patches/thy_output.ML}),
|
||||
\<^item> \<^isadof> has been organized as an AFP entry and a form of an Isabelle component that is
|
||||
compatible with this goal,
|
||||
\<^item> we decided to make the markup-generation by itself to adapt it as well as possible to the
|
||||
needs of tracking the linking in documents,
|
||||
\<^item> \<^isadof> is deeply integrated into the Isabelle's IDE (PIDE) to give immediate feedback during
|
||||
|
@ -95,10 +95,11 @@ op repeat : ('a -> 'b * 'a) -> 'a -> 'b list * 'a \<close>}
|
|||
for alternative, sequence, and piping, as well as combinators for option and repeat. Parsing
|
||||
combinators have the advantage that they can be integrated into standard programs,
|
||||
and they enable the dynamic extension of the grammar. There is a more high-level structure
|
||||
\inlinesml{Parse} providing specific combinators for the command-language Isar:
|
||||
\<^boxed_sml>\<open>Parse\<close> providing specific combinators for the command-language Isar:
|
||||
|
||||
\begin{sml}[mathescape=false]
|
||||
val attribute = Parse.position Parse.name
|
||||
% boxed_sml does not work here due to the dollar symbols. Repair: mathescape option in sty ?
|
||||
@{boxed_sml [display]
|
||||
\<open>val attribute = Parse.position Parse.name
|
||||
-- Scan.optional(Parse.$$$ "=" |-- Parse.!!! Parse.name)"";
|
||||
val reference = Parse.position Parse.name
|
||||
-- Scan.option (Parse.$$$ "::" |-- Parse.!!!
|
||||
|
@ -106,7 +107,7 @@ val reference = Parse.position Parse.name
|
|||
val attributes =(Parse.$$$ "[" |-- (reference
|
||||
-- (Scan.optional(Parse.$$$ ","
|
||||
|--(Parse.enum ","attribute)))[]))--| Parse.$$$ "]"
|
||||
\end{sml}
|
||||
\<close>}
|
||||
|
||||
The ``model'' \<^boxed_sml>\<open>create_and_check_docitem\<close> and ``new''
|
||||
\<^boxed_sml>\<open>ODL_Meta_Args_Parser.attributes\<close> parts were
|
||||
|
@ -171,7 +172,7 @@ section\<open>Implementing Second-level Type-Checking\<close>
|
|||
text\<open>
|
||||
On expressions for attribute values, for which we chose to use HOL syntax to avoid that users
|
||||
need to learn another syntax, we implemented an own pass over type-checked terms. Stored in the
|
||||
late-binding table \<^boxed_sml>\<open>ISA_transformer_tab\<close>, we register for each inner-syntax-annotation
|
||||
late-binding table \<^boxed_sml>\<open>ISA_transformer_tab\<close>, we register for each term-annotation
|
||||
(ISA's), a function of type
|
||||
|
||||
@{boxed_sml [display]
|
||||
|
|
Loading…
Reference in New Issue