Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

recvision till line 2000 (Term Parsing)

This commit is contained in:
Burkhart Wolff 2020-10-21 13:49:01 +02:00
parent 9b2c08183e
commit 7999ee9a38
1 changed files with 11 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy
View File

@ -2005,21 +2005,16 @@ text\<open>
text\<open> text\<open>
Note that @{ML "Syntax.install_operations"} is a late-binding interface, i.e. a collection of Note that \<^ML>\<open>Syntax.install_operations\<close> is a late-binding interface, i.e. a collection of
"hooks" used to resolve an apparent architectural cycle. "hooks" used to resolve an apparent architectural cycle.
The real work is done in @{file "~~/src/Pure/Syntax/syntax_phases.ML"} The real work is done in \<^file>\<open>~~/src/Pure/Syntax/syntax_phases.ML\<close>
Even the parsers and type checkers stemming from the theory-structure are registered via Even the parsers and type checkers stemming from the theory-structure are registered via
hooks (this can be confusing at times). Main phases of inner syntax processing, with standard hooks (this can be confusing at times). Main phases of inner syntax processing, with standard
implementations of parse/unparse operations were treated this way. implementations of parse/unparse operations were treated this way.
At the very very end in , it sets up the entire syntax engine At the very very end in, it sets up the entire syntax engine (the hooks) via:
(the hooks) via:
\<close>
\<^theory_text>\<open>Theory.setup
(*
val _ =
Theory.setup
(Syntax.install_operations (Syntax.install_operations
{parse_sort = parse_sort, {parse_sort = parse_sort,
parse_typ = parse_typ, parse_typ = parse_typ,
@ -2032,8 +2027,11 @@ val _ =
check_terms = check_terms, check_terms = check_terms,
check_props = check_props, check_props = check_props,
uncheck_typs = uncheck_typs, uncheck_typs = uncheck_typs,
uncheck_terms = uncheck_terms}); uncheck_terms = uncheck_terms})
*) \<close>
\<close>
subsection*[ex33::example] \<open>Example\<close> subsection*[ex33::example] \<open>Example\<close>
@ -2086,7 +2084,7 @@ Output.output "bla_1:";
text\<open>It provides a number of hooks that can be used for redirection hacks ...\<close> text\<open>It provides a number of hooks that can be used for redirection hacks ...\<close>
section \<open> Output: LaTeX \<close> section \<open> Output: LaTeX \<close>
text\<open>The heart of the LaTeX generator is to be found in the structure @{ML_structure Thy_Output}. text\<open>The heart of the LaTeX generator is to be found in the structure \<^ML_structure>\<open>Thy_Output\<close>.
This is an own parsing and writing process, with the risc that a parsed file in the IDE parsing This is an own parsing and writing process, with the risc that a parsed file in the IDE parsing
process can not be parsed for the LaTeX Generator. The reason is twofold: process can not be parsed for the LaTeX Generator. The reason is twofold:
\<^enum> The LaTeX Generator makes a rough attempt to mimic the LayOut if the thy-file; thus, its \<^enum> The LaTeX Generator makes a rough attempt to mimic the LayOut if the thy-file; thus, its
@ -2096,7 +2094,7 @@ text\<open>The heart of the LaTeX generator is to be found in the structure @{ML
called @{ML "Document_Source.improper"} where also other forms of comment parsers are provided. called @{ML "Document_Source.improper"} where also other forms of comment parsers are provided.
Since Isabelle2018, an own AST is provided for the LaTeX syntax, analogously to Since Isabelle2018, an own AST is provided for the LaTeX syntax, analogously to
@{ML_structure "Pretty"}. Key functions of this structure @{ML_structure "Latex"} are: \<^ML_structure>\<open>Pretty\<close>. Key functions of this structure \<^ML_structure>\<open>Latex\<close> are:
\<close> \<close>
ML\<open> ML\<open>