diff --git a/src/Doc/Main/Main_Doc.thy b/src/Doc/Main/Main_Doc.thy --- a/src/Doc/Main/Main_Doc.thy +++ b/src/Doc/Main/Main_Doc.thy @@ -1,650 +1,650 @@ (*<*) theory Main_Doc imports Main begin setup \ - Thy_Output.antiquotation_pretty_source \<^binding>\term_type_only\ (Args.term -- Args.typ_abbrev) + Document_Output.antiquotation_pretty_source \<^binding>\term_type_only\ (Args.term -- Args.typ_abbrev) (fn ctxt => fn (t, T) => (if fastype_of t = Sign.certify_typ (Proof_Context.theory_of ctxt) T then () else error "term_type_only: type mismatch"; Syntax.pretty_typ ctxt T)) \ setup \ - Thy_Output.antiquotation_pretty_source \<^binding>\expanded_typ\ Args.typ + Document_Output.antiquotation_pretty_source \<^binding>\expanded_typ\ Args.typ Syntax.pretty_typ \ (*>*) text\ \begin{abstract} This document lists the main types, functions and syntax provided by theory \<^theory>\Main\. It is meant as a quick overview of what is available. For infix operators and their precedences see the final section. The sophisticated class structure is only hinted at. For details see \<^url>\https://isabelle.in.tum.de/library/HOL\. \end{abstract} \section*{HOL} The basic logic: \<^prop>\x = y\, \<^const>\True\, \<^const>\False\, \<^prop>\\ P\, \<^prop>\P \ Q\, \<^prop>\P \ Q\, \<^prop>\P \ Q\, \<^prop>\\x. P\, \<^prop>\\x. P\, \<^prop>\\! x. P\, \<^term>\THE x. P\. \<^smallskip> \begin{tabular}{@ {} l @ {~::~} l @ {}} \<^const>\HOL.undefined\ & \<^typeof>\HOL.undefined\\\ \<^const>\HOL.default\ & \<^typeof>\HOL.default\\\ \end{tabular} \subsubsection*{Syntax} \begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} \<^term>\\ (x = y)\ & @{term[source]"\ (x = y)"} & (\<^verbatim>\~=\)\\ @{term[source]"P \ Q"} & \<^term>\P \ Q\ \\ \<^term>\If x y z\ & @{term[source]"If x y z"}\\ \<^term>\Let e\<^sub>1 (\x. e\<^sub>2)\ & @{term[source]"Let e\<^sub>1 (\x. e\<^sub>2)"}\\ \end{supertabular} \section*{Orderings} A collection of classes defining basic orderings: preorder, partial order, linear order, dense linear order and wellorder. \<^smallskip> \begin{supertabular}{@ {} l @ {~::~} l l @ {}} \<^const>\Orderings.less_eq\ & \<^typeof>\Orderings.less_eq\ & (\<^verbatim>\<=\)\\ \<^const>\Orderings.less\ & \<^typeof>\Orderings.less\\\ \<^const>\Orderings.Least\ & \<^typeof>\Orderings.Least\\\ \<^const>\Orderings.Greatest\ & \<^typeof>\Orderings.Greatest\\\ \<^const>\Orderings.min\ & \<^typeof>\Orderings.min\\\ \<^const>\Orderings.max\ & \<^typeof>\Orderings.max\\\ @{const[source] top} & \<^typeof>\Orderings.top\\\ @{const[source] bot} & \<^typeof>\Orderings.bot\\\ \<^const>\Orderings.mono\ & \<^typeof>\Orderings.mono\\\ \<^const>\Orderings.strict_mono\ & \<^typeof>\Orderings.strict_mono\\\ \end{supertabular} \subsubsection*{Syntax} \begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} @{term[source]"x \ y"} & \<^term>\x \ y\ & (\<^verbatim>\>=\)\\ @{term[source]"x > y"} & \<^term>\x > y\\\ \<^term>\\x\y. P\ & @{term[source]"\x. x \ y \ P"}\\ \<^term>\\x\y. P\ & @{term[source]"\x. x \ y \ P"}\\ \multicolumn{2}{@ {}l@ {}}{Similarly for $<$, $\ge$ and $>$}\\ \<^term>\LEAST x. P\ & @{term[source]"Least (\x. P)"}\\ \<^term>\GREATEST x. P\ & @{term[source]"Greatest (\x. P)"}\\ \end{supertabular} \section*{Lattices} Classes semilattice, lattice, distributive lattice and complete lattice (the latter in theory \<^theory>\HOL.Set\). \begin{tabular}{@ {} l @ {~::~} l @ {}} \<^const>\Lattices.inf\ & \<^typeof>\Lattices.inf\\\ \<^const>\Lattices.sup\ & \<^typeof>\Lattices.sup\\\ \<^const>\Complete_Lattices.Inf\ & @{term_type_only Complete_Lattices.Inf "'a set \ 'a::Inf"}\\ \<^const>\Complete_Lattices.Sup\ & @{term_type_only Complete_Lattices.Sup "'a set \ 'a::Sup"}\\ \end{tabular} \subsubsection*{Syntax} Available by loading theory \Lattice_Syntax\ in directory \Library\. \begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} @{text[source]"x \ y"} & \<^term>\x \ y\\\ @{text[source]"x \ y"} & \<^term>\x < y\\\ @{text[source]"x \ y"} & \<^term>\inf x y\\\ @{text[source]"x \ y"} & \<^term>\sup x y\\\ @{text[source]"\A"} & \<^term>\Inf A\\\ @{text[source]"\A"} & \<^term>\Sup A\\\ @{text[source]"\"} & @{term[source] top}\\ @{text[source]"\"} & @{term[source] bot}\\ \end{supertabular} \section*{Set} \begin{supertabular}{@ {} l @ {~::~} l l @ {}} \<^const>\Set.empty\ & @{term_type_only "Set.empty" "'a set"}\\ \<^const>\Set.insert\ & @{term_type_only insert "'a\'a set\'a set"}\\ \<^const>\Collect\ & @{term_type_only Collect "('a\bool)\'a set"}\\ \<^const>\Set.member\ & @{term_type_only Set.member "'a\'a set\bool"} & (\<^verbatim>\:\)\\ \<^const>\Set.union\ & @{term_type_only Set.union "'a set\'a set \ 'a set"} & (\<^verbatim>\Un\)\\ \<^const>\Set.inter\ & @{term_type_only Set.inter "'a set\'a set \ 'a set"} & (\<^verbatim>\Int\)\\ \<^const>\Union\ & @{term_type_only Union "'a set set\'a set"}\\ \<^const>\Inter\ & @{term_type_only Inter "'a set set\'a set"}\\ \<^const>\Pow\ & @{term_type_only Pow "'a set \'a set set"}\\ \<^const>\UNIV\ & @{term_type_only UNIV "'a set"}\\ \<^const>\image\ & @{term_type_only image "('a\'b)\'a set\'b set"}\\ \<^const>\Ball\ & @{term_type_only Ball "'a set\('a\bool)\bool"}\\ \<^const>\Bex\ & @{term_type_only Bex "'a set\('a\bool)\bool"}\\ \end{supertabular} \subsubsection*{Syntax} \begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} \{a\<^sub>1,\,a\<^sub>n}\ & \insert a\<^sub>1 (\ (insert a\<^sub>n {})\)\\\ \<^term>\a \ A\ & @{term[source]"\(x \ A)"}\\ \<^term>\A \ B\ & @{term[source]"A \ B"}\\ \<^term>\A \ B\ & @{term[source]"A < B"}\\ @{term[source]"A \ B"} & @{term[source]"B \ A"}\\ @{term[source]"A \ B"} & @{term[source]"B < A"}\\ \<^term>\{x. P}\ & @{term[source]"Collect (\x. P)"}\\ \{t | x\<^sub>1 \ x\<^sub>n. P}\ & \{v. \x\<^sub>1 \ x\<^sub>n. v = t \ P}\\\ @{term[source]"\x\I. A"} & @{term[source]"\((\x. A) ` I)"} & (\texttt{UN})\\ @{term[source]"\x. A"} & @{term[source]"\((\x. A) ` UNIV)"}\\ @{term[source]"\x\I. A"} & @{term[source]"\((\x. A) ` I)"} & (\texttt{INT})\\ @{term[source]"\x. A"} & @{term[source]"\((\x. A) ` UNIV)"}\\ \<^term>\\x\A. P\ & @{term[source]"Ball A (\x. P)"}\\ \<^term>\\x\A. P\ & @{term[source]"Bex A (\x. P)"}\\ \<^term>\range f\ & @{term[source]"f ` UNIV"}\\ \end{supertabular} \section*{Fun} \begin{supertabular}{@ {} l @ {~::~} l l @ {}} \<^const>\Fun.id\ & \<^typeof>\Fun.id\\\ \<^const>\Fun.comp\ & \<^typeof>\Fun.comp\ & (\texttt{o})\\ \<^const>\Fun.inj_on\ & @{term_type_only Fun.inj_on "('a\'b)\'a set\bool"}\\ \<^const>\Fun.inj\ & \<^typeof>\Fun.inj\\\ \<^const>\Fun.surj\ & \<^typeof>\Fun.surj\\\ \<^const>\Fun.bij\ & \<^typeof>\Fun.bij\\\ \<^const>\Fun.bij_betw\ & @{term_type_only Fun.bij_betw "('a\'b)\'a set\'b set\bool"}\\ \<^const>\Fun.fun_upd\ & \<^typeof>\Fun.fun_upd\\\ \end{supertabular} \subsubsection*{Syntax} \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} \<^term>\fun_upd f x y\ & @{term[source]"fun_upd f x y"}\\ \f(x\<^sub>1:=y\<^sub>1,\,x\<^sub>n:=y\<^sub>n)\ & \f(x\<^sub>1:=y\<^sub>1)\(x\<^sub>n:=y\<^sub>n)\\\ \end{tabular} \section*{Hilbert\_Choice} Hilbert's selection ($\varepsilon$) operator: \<^term>\SOME x. P\. \<^smallskip> \begin{tabular}{@ {} l @ {~::~} l @ {}} \<^const>\Hilbert_Choice.inv_into\ & @{term_type_only Hilbert_Choice.inv_into "'a set \ ('a \ 'b) \ ('b \ 'a)"} \end{tabular} \subsubsection*{Syntax} \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} \<^term>\inv\ & @{term[source]"inv_into UNIV"} \end{tabular} \section*{Fixed Points} Theory: \<^theory>\HOL.Inductive\. Least and greatest fixed points in a complete lattice \<^typ>\'a\: \begin{tabular}{@ {} l @ {~::~} l @ {}} \<^const>\Inductive.lfp\ & \<^typeof>\Inductive.lfp\\\ \<^const>\Inductive.gfp\ & \<^typeof>\Inductive.gfp\\\ \end{tabular} Note that in particular sets (\<^typ>\'a \ bool\) are complete lattices. \section*{Sum\_Type} Type constructor \+\. \begin{tabular}{@ {} l @ {~::~} l @ {}} \<^const>\Sum_Type.Inl\ & \<^typeof>\Sum_Type.Inl\\\ \<^const>\Sum_Type.Inr\ & \<^typeof>\Sum_Type.Inr\\\ \<^const>\Sum_Type.Plus\ & @{term_type_only Sum_Type.Plus "'a set\'b set\('a+'b)set"} \end{tabular} \section*{Product\_Type} Types \<^typ>\unit\ and \\\. \begin{supertabular}{@ {} l @ {~::~} l @ {}} \<^const>\Product_Type.Unity\ & \<^typeof>\Product_Type.Unity\\\ \<^const>\Pair\ & \<^typeof>\Pair\\\ \<^const>\fst\ & \<^typeof>\fst\\\ \<^const>\snd\ & \<^typeof>\snd\\\ \<^const>\case_prod\ & \<^typeof>\case_prod\\\ \<^const>\curry\ & \<^typeof>\curry\\\ \<^const>\Product_Type.Sigma\ & @{term_type_only Product_Type.Sigma "'a set\('a\'b set)\('a*'b)set"}\\ \end{supertabular} \subsubsection*{Syntax} \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} ll @ {}} \<^term>\Pair a b\ & @{term[source]"Pair a b"}\\ \<^term>\case_prod (\x y. t)\ & @{term[source]"case_prod (\x y. t)"}\\ \<^term>\A \ B\ & \Sigma A (\\<^latex>\\_\. B)\ \end{tabular} Pairs may be nested. Nesting to the right is printed as a tuple, e.g.\ \mbox{\<^term>\(a,b,c)\} is really \mbox{\(a, (b, c))\.} Pattern matching with pairs and tuples extends to all binders, e.g.\ \mbox{\<^prop>\\(x,y)\A. P\,} \<^term>\{(x,y). P}\, etc. \section*{Relation} \begin{tabular}{@ {} l @ {~::~} l @ {}} \<^const>\Relation.converse\ & @{term_type_only Relation.converse "('a * 'b)set \ ('b*'a)set"}\\ \<^const>\Relation.relcomp\ & @{term_type_only Relation.relcomp "('a*'b)set\('b*'c)set\('a*'c)set"}\\ \<^const>\Relation.Image\ & @{term_type_only Relation.Image "('a*'b)set\'a set\'b set"}\\ \<^const>\Relation.inv_image\ & @{term_type_only Relation.inv_image "('a*'a)set\('b\'a)\('b*'b)set"}\\ \<^const>\Relation.Id_on\ & @{term_type_only Relation.Id_on "'a set\('a*'a)set"}\\ \<^const>\Relation.Id\ & @{term_type_only Relation.Id "('a*'a)set"}\\ \<^const>\Relation.Domain\ & @{term_type_only Relation.Domain "('a*'b)set\'a set"}\\ \<^const>\Relation.Range\ & @{term_type_only Relation.Range "('a*'b)set\'b set"}\\ \<^const>\Relation.Field\ & @{term_type_only Relation.Field "('a*'a)set\'a set"}\\ \<^const>\Relation.refl_on\ & @{term_type_only Relation.refl_on "'a set\('a*'a)set\bool"}\\ \<^const>\Relation.refl\ & @{term_type_only Relation.refl "('a*'a)set\bool"}\\ \<^const>\Relation.sym\ & @{term_type_only Relation.sym "('a*'a)set\bool"}\\ \<^const>\Relation.antisym\ & @{term_type_only Relation.antisym "('a*'a)set\bool"}\\ \<^const>\Relation.trans\ & @{term_type_only Relation.trans "('a*'a)set\bool"}\\ \<^const>\Relation.irrefl\ & @{term_type_only Relation.irrefl "('a*'a)set\bool"}\\ \<^const>\Relation.total_on\ & @{term_type_only Relation.total_on "'a set\('a*'a)set\bool"}\\ \<^const>\Relation.total\ & @{term_type_only Relation.total "('a*'a)set\bool"}\\ \end{tabular} \subsubsection*{Syntax} \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} \<^term>\converse r\ & @{term[source]"converse r"} & (\<^verbatim>\^-1\) \end{tabular} \<^medskip> \noindent Type synonym \ \<^typ>\'a rel\ \=\ @{expanded_typ "'a rel"} \section*{Equiv\_Relations} \begin{supertabular}{@ {} l @ {~::~} l @ {}} \<^const>\Equiv_Relations.equiv\ & @{term_type_only Equiv_Relations.equiv "'a set \ ('a*'a)set\bool"}\\ \<^const>\Equiv_Relations.quotient\ & @{term_type_only Equiv_Relations.quotient "'a set \ ('a \ 'a) set \ 'a set set"}\\ \<^const>\Equiv_Relations.congruent\ & @{term_type_only Equiv_Relations.congruent "('a*'a)set\('a\'b)\bool"}\\ \<^const>\Equiv_Relations.congruent2\ & @{term_type_only Equiv_Relations.congruent2 "('a*'a)set\('b*'b)set\('a\'b\'c)\bool"}\\ %@ {const Equiv_Relations.} & @ {term_type_only Equiv_Relations. ""}\\ \end{supertabular} \subsubsection*{Syntax} \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} \<^term>\congruent r f\ & @{term[source]"congruent r f"}\\ \<^term>\congruent2 r r f\ & @{term[source]"congruent2 r r f"}\\ \end{tabular} \section*{Transitive\_Closure} \begin{tabular}{@ {} l @ {~::~} l @ {}} \<^const>\Transitive_Closure.rtrancl\ & @{term_type_only Transitive_Closure.rtrancl "('a*'a)set\('a*'a)set"}\\ \<^const>\Transitive_Closure.trancl\ & @{term_type_only Transitive_Closure.trancl "('a*'a)set\('a*'a)set"}\\ \<^const>\Transitive_Closure.reflcl\ & @{term_type_only Transitive_Closure.reflcl "('a*'a)set\('a*'a)set"}\\ \<^const>\Transitive_Closure.acyclic\ & @{term_type_only Transitive_Closure.acyclic "('a*'a)set\bool"}\\ \<^const>\compower\ & @{term_type_only "(^^) :: ('a*'a)set\nat\('a*'a)set" "('a*'a)set\nat\('a*'a)set"}\\ \end{tabular} \subsubsection*{Syntax} \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} \<^term>\rtrancl r\ & @{term[source]"rtrancl r"} & (\<^verbatim>\^*\)\\ \<^term>\trancl r\ & @{term[source]"trancl r"} & (\<^verbatim>\^+\)\\ \<^term>\reflcl r\ & @{term[source]"reflcl r"} & (\<^verbatim>\^=\) \end{tabular} \section*{Algebra} Theories \<^theory>\HOL.Groups\, \<^theory>\HOL.Rings\, \<^theory>\HOL.Fields\ and \<^theory>\HOL.Divides\ define a large collection of classes describing common algebraic structures from semigroups up to fields. Everything is done in terms of overloaded operators: \begin{supertabular}{@ {} l @ {~::~} l l @ {}} \0\ & \<^typeof>\zero\\\ \1\ & \<^typeof>\one\\\ \<^const>\plus\ & \<^typeof>\plus\\\ \<^const>\minus\ & \<^typeof>\minus\\\ \<^const>\uminus\ & \<^typeof>\uminus\ & (\<^verbatim>\-\)\\ \<^const>\times\ & \<^typeof>\times\\\ \<^const>\inverse\ & \<^typeof>\inverse\\\ \<^const>\divide\ & \<^typeof>\divide\\\ \<^const>\abs\ & \<^typeof>\abs\\\ \<^const>\sgn\ & \<^typeof>\sgn\\\ \<^const>\Rings.dvd\ & \<^typeof>\Rings.dvd\\\ \<^const>\divide\ & \<^typeof>\divide\\\ \<^const>\modulo\ & \<^typeof>\modulo\\\ \end{supertabular} \subsubsection*{Syntax} \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} \<^term>\\x\\ & @{term[source] "abs x"} \end{tabular} \section*{Nat} \<^datatype>\nat\ \<^bigskip> \begin{tabular}{@ {} lllllll @ {}} \<^term>\(+) :: nat \ nat \ nat\ & \<^term>\(-) :: nat \ nat \ nat\ & \<^term>\(*) :: nat \ nat \ nat\ & \<^term>\(^) :: nat \ nat \ nat\ & \<^term>\(div) :: nat \ nat \ nat\& \<^term>\(mod) :: nat \ nat \ nat\& \<^term>\(dvd) :: nat \ nat \ bool\\\ \<^term>\(\) :: nat \ nat \ bool\ & \<^term>\(<) :: nat \ nat \ bool\ & \<^term>\min :: nat \ nat \ nat\ & \<^term>\max :: nat \ nat \ nat\ & \<^term>\Min :: nat set \ nat\ & \<^term>\Max :: nat set \ nat\\\ \end{tabular} \begin{tabular}{@ {} l @ {~::~} l @ {}} \<^const>\Nat.of_nat\ & \<^typeof>\Nat.of_nat\\\ \<^term>\(^^) :: ('a \ 'a) \ nat \ 'a \ 'a\ & @{term_type_only "(^^) :: ('a \ 'a) \ nat \ 'a \ 'a" "('a \ 'a) \ nat \ 'a \ 'a"} \end{tabular} \section*{Int} Type \<^typ>\int\ \<^bigskip> \begin{tabular}{@ {} llllllll @ {}} \<^term>\(+) :: int \ int \ int\ & \<^term>\(-) :: int \ int \ int\ & \<^term>\uminus :: int \ int\ & \<^term>\(*) :: int \ int \ int\ & \<^term>\(^) :: int \ nat \ int\ & \<^term>\(div) :: int \ int \ int\& \<^term>\(mod) :: int \ int \ int\& \<^term>\(dvd) :: int \ int \ bool\\\ \<^term>\(\) :: int \ int \ bool\ & \<^term>\(<) :: int \ int \ bool\ & \<^term>\min :: int \ int \ int\ & \<^term>\max :: int \ int \ int\ & \<^term>\Min :: int set \ int\ & \<^term>\Max :: int set \ int\\\ \<^term>\abs :: int \ int\ & \<^term>\sgn :: int \ int\\\ \end{tabular} \begin{tabular}{@ {} l @ {~::~} l l @ {}} \<^const>\Int.nat\ & \<^typeof>\Int.nat\\\ \<^const>\Int.of_int\ & \<^typeof>\Int.of_int\\\ \<^const>\Int.Ints\ & @{term_type_only Int.Ints "'a::ring_1 set"} & (\<^verbatim>\Ints\) \end{tabular} \subsubsection*{Syntax} \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} \<^term>\of_nat::nat\int\ & @{term[source]"of_nat"}\\ \end{tabular} \section*{Finite\_Set} \begin{supertabular}{@ {} l @ {~::~} l @ {}} \<^const>\Finite_Set.finite\ & @{term_type_only Finite_Set.finite "'a set\bool"}\\ \<^const>\Finite_Set.card\ & @{term_type_only Finite_Set.card "'a set \ nat"}\\ \<^const>\Finite_Set.fold\ & @{term_type_only Finite_Set.fold "('a \ 'b \ 'b) \ 'b \ 'a set \ 'b"}\\ \end{supertabular} \section*{Lattices\_Big} \begin{supertabular}{@ {} l @ {~::~} l l @ {}} \<^const>\Lattices_Big.Min\ & \<^typeof>\Lattices_Big.Min\\\ \<^const>\Lattices_Big.Max\ & \<^typeof>\Lattices_Big.Max\\\ \<^const>\Lattices_Big.arg_min\ & \<^typeof>\Lattices_Big.arg_min\\\ \<^const>\Lattices_Big.is_arg_min\ & \<^typeof>\Lattices_Big.is_arg_min\\\ \<^const>\Lattices_Big.arg_max\ & \<^typeof>\Lattices_Big.arg_max\\\ \<^const>\Lattices_Big.is_arg_max\ & \<^typeof>\Lattices_Big.is_arg_max\\\ \end{supertabular} \subsubsection*{Syntax} \begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} \<^term>\ARG_MIN f x. P\ & @{term[source]"arg_min f (\x. P)"}\\ \<^term>\ARG_MAX f x. P\ & @{term[source]"arg_max f (\x. P)"}\\ \end{supertabular} \section*{Groups\_Big} \begin{supertabular}{@ {} l @ {~::~} l @ {}} \<^const>\Groups_Big.sum\ & @{term_type_only Groups_Big.sum "('a \ 'b) \ 'a set \ 'b::comm_monoid_add"}\\ \<^const>\Groups_Big.prod\ & @{term_type_only Groups_Big.prod "('a \ 'b) \ 'a set \ 'b::comm_monoid_mult"}\\ \end{supertabular} \subsubsection*{Syntax} \begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} \<^term>\sum (\x. x) A\ & @{term[source]"sum (\x. x) A"} & (\<^verbatim>\SUM\)\\ \<^term>\sum (\x. t) A\ & @{term[source]"sum (\x. t) A"}\\ @{term[source] "\x|P. t"} & \<^term>\\x|P. t\\\ \multicolumn{2}{@ {}l@ {}}{Similarly for \\\ instead of \\\} & (\<^verbatim>\PROD\)\\ \end{supertabular} \section*{Wellfounded} \begin{supertabular}{@ {} l @ {~::~} l @ {}} \<^const>\Wellfounded.wf\ & @{term_type_only Wellfounded.wf "('a*'a)set\bool"}\\ \<^const>\Wellfounded.acc\ & @{term_type_only Wellfounded.acc "('a*'a)set\'a set"}\\ \<^const>\Wellfounded.measure\ & @{term_type_only Wellfounded.measure "('a\nat)\('a*'a)set"}\\ \<^const>\Wellfounded.lex_prod\ & @{term_type_only Wellfounded.lex_prod "('a*'a)set\('b*'b)set\(('a*'b)*('a*'b))set"}\\ \<^const>\Wellfounded.mlex_prod\ & @{term_type_only Wellfounded.mlex_prod "('a\nat)\('a*'a)set\('a*'a)set"}\\ \<^const>\Wellfounded.less_than\ & @{term_type_only Wellfounded.less_than "(nat*nat)set"}\\ \<^const>\Wellfounded.pred_nat\ & @{term_type_only Wellfounded.pred_nat "(nat*nat)set"}\\ \end{supertabular} \section*{Set\_Interval} % \<^theory>\HOL.Set_Interval\ \begin{supertabular}{@ {} l @ {~::~} l @ {}} \<^const>\lessThan\ & @{term_type_only lessThan "'a::ord \ 'a set"}\\ \<^const>\atMost\ & @{term_type_only atMost "'a::ord \ 'a set"}\\ \<^const>\greaterThan\ & @{term_type_only greaterThan "'a::ord \ 'a set"}\\ \<^const>\atLeast\ & @{term_type_only atLeast "'a::ord \ 'a set"}\\ \<^const>\greaterThanLessThan\ & @{term_type_only greaterThanLessThan "'a::ord \ 'a \ 'a set"}\\ \<^const>\atLeastLessThan\ & @{term_type_only atLeastLessThan "'a::ord \ 'a \ 'a set"}\\ \<^const>\greaterThanAtMost\ & @{term_type_only greaterThanAtMost "'a::ord \ 'a \ 'a set"}\\ \<^const>\atLeastAtMost\ & @{term_type_only atLeastAtMost "'a::ord \ 'a \ 'a set"}\\ \end{supertabular} \subsubsection*{Syntax} \begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} \<^term>\lessThan y\ & @{term[source] "lessThan y"}\\ \<^term>\atMost y\ & @{term[source] "atMost y"}\\ \<^term>\greaterThan x\ & @{term[source] "greaterThan x"}\\ \<^term>\atLeast x\ & @{term[source] "atLeast x"}\\ \<^term>\greaterThanLessThan x y\ & @{term[source] "greaterThanLessThan x y"}\\ \<^term>\atLeastLessThan x y\ & @{term[source] "atLeastLessThan x y"}\\ \<^term>\greaterThanAtMost x y\ & @{term[source] "greaterThanAtMost x y"}\\ \<^term>\atLeastAtMost x y\ & @{term[source] "atLeastAtMost x y"}\\ @{term[source] "\i\n. A"} & @{term[source] "\i \ {..n}. A"}\\ @{term[source] "\ii \ {..\\ instead of \\\}\\ \<^term>\sum (\x. t) {a..b}\ & @{term[source] "sum (\x. t) {a..b}"}\\ \<^term>\sum (\x. t) {a.. & @{term[source] "sum (\x. t) {a..\sum (\x. t) {..b}\ & @{term[source] "sum (\x. t) {..b}"}\\ \<^term>\sum (\x. t) {.. & @{term[source] "sum (\x. t) {..\\ instead of \\\}\\ \end{supertabular} \section*{Power} \begin{tabular}{@ {} l @ {~::~} l @ {}} \<^const>\Power.power\ & \<^typeof>\Power.power\ \end{tabular} \section*{Option} \<^datatype>\option\ \<^bigskip> \begin{tabular}{@ {} l @ {~::~} l @ {}} \<^const>\Option.the\ & \<^typeof>\Option.the\\\ \<^const>\map_option\ & @{typ[source]"('a \ 'b) \ 'a option \ 'b option"}\\ \<^const>\set_option\ & @{term_type_only set_option "'a option \ 'a set"}\\ \<^const>\Option.bind\ & @{term_type_only Option.bind "'a option \ ('a \ 'b option) \ 'b option"} \end{tabular} \section*{List} \<^datatype>\list\ \<^bigskip> \begin{supertabular}{@ {} l @ {~::~} l @ {}} \<^const>\List.append\ & \<^typeof>\List.append\\\ \<^const>\List.butlast\ & \<^typeof>\List.butlast\\\ \<^const>\List.concat\ & \<^typeof>\List.concat\\\ \<^const>\List.distinct\ & \<^typeof>\List.distinct\\\ \<^const>\List.drop\ & \<^typeof>\List.drop\\\ \<^const>\List.dropWhile\ & \<^typeof>\List.dropWhile\\\ \<^const>\List.filter\ & \<^typeof>\List.filter\\\ \<^const>\List.find\ & \<^typeof>\List.find\\\ \<^const>\List.fold\ & \<^typeof>\List.fold\\\ \<^const>\List.foldr\ & \<^typeof>\List.foldr\\\ \<^const>\List.foldl\ & \<^typeof>\List.foldl\\\ \<^const>\List.hd\ & \<^typeof>\List.hd\\\ \<^const>\List.last\ & \<^typeof>\List.last\\\ \<^const>\List.length\ & \<^typeof>\List.length\\\ \<^const>\List.lenlex\ & @{term_type_only List.lenlex "('a*'a)set\('a list * 'a list)set"}\\ \<^const>\List.lex\ & @{term_type_only List.lex "('a*'a)set\('a list * 'a list)set"}\\ \<^const>\List.lexn\ & @{term_type_only List.lexn "('a*'a)set\nat\('a list * 'a list)set"}\\ \<^const>\List.lexord\ & @{term_type_only List.lexord "('a*'a)set\('a list * 'a list)set"}\\ \<^const>\List.listrel\ & @{term_type_only List.listrel "('a*'b)set\('a list * 'b list)set"}\\ \<^const>\List.listrel1\ & @{term_type_only List.listrel1 "('a*'a)set\('a list * 'a list)set"}\\ \<^const>\List.lists\ & @{term_type_only List.lists "'a set\'a list set"}\\ \<^const>\List.listset\ & @{term_type_only List.listset "'a set list \ 'a list set"}\\ \<^const>\Groups_List.sum_list\ & \<^typeof>\Groups_List.sum_list\\\ \<^const>\Groups_List.prod_list\ & \<^typeof>\Groups_List.prod_list\\\ \<^const>\List.list_all2\ & \<^typeof>\List.list_all2\\\ \<^const>\List.list_update\ & \<^typeof>\List.list_update\\\ \<^const>\List.map\ & \<^typeof>\List.map\\\ \<^const>\List.measures\ & @{term_type_only List.measures "('a\nat)list\('a*'a)set"}\\ \<^const>\List.nth\ & \<^typeof>\List.nth\\\ \<^const>\List.nths\ & \<^typeof>\List.nths\\\ \<^const>\List.remdups\ & \<^typeof>\List.remdups\\\ \<^const>\List.removeAll\ & \<^typeof>\List.removeAll\\\ \<^const>\List.remove1\ & \<^typeof>\List.remove1\\\ \<^const>\List.replicate\ & \<^typeof>\List.replicate\\\ \<^const>\List.rev\ & \<^typeof>\List.rev\\\ \<^const>\List.rotate\ & \<^typeof>\List.rotate\\\ \<^const>\List.rotate1\ & \<^typeof>\List.rotate1\\\ \<^const>\List.set\ & @{term_type_only List.set "'a list \ 'a set"}\\ \<^const>\List.shuffles\ & \<^typeof>\List.shuffles\\\ \<^const>\List.sort\ & \<^typeof>\List.sort\\\ \<^const>\List.sorted\ & \<^typeof>\List.sorted\\\ \<^const>\List.sorted_wrt\ & \<^typeof>\List.sorted_wrt\\\ \<^const>\List.splice\ & \<^typeof>\List.splice\\\ \<^const>\List.take\ & \<^typeof>\List.take\\\ \<^const>\List.takeWhile\ & \<^typeof>\List.takeWhile\\\ \<^const>\List.tl\ & \<^typeof>\List.tl\\\ \<^const>\List.upt\ & \<^typeof>\List.upt\\\ \<^const>\List.upto\ & \<^typeof>\List.upto\\\ \<^const>\List.zip\ & \<^typeof>\List.zip\\\ \end{supertabular} \subsubsection*{Syntax} \begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} \[x\<^sub>1,\,x\<^sub>n]\ & \x\<^sub>1 # \ # x\<^sub>n # []\\\ \<^term>\[m.. & @{term[source]"upt m n"}\\ \<^term>\[i..j]\ & @{term[source]"upto i j"}\\ \<^term>\xs[n := x]\ & @{term[source]"list_update xs n x"}\\ \<^term>\\x\xs. e\ & @{term[source]"listsum (map (\x. e) xs)"}\\ \end{supertabular} \<^medskip> Filter input syntax \[pat \ e. b]\, where \pat\ is a tuple pattern, which stands for \<^term>\filter (\pat. b) e\. List comprehension input syntax: \[e. q\<^sub>1, \, q\<^sub>n]\ where each qualifier \q\<^sub>i\ is either a generator \mbox{\pat \ e\} or a guard, i.e.\ boolean expression. \section*{Map} Maps model partial functions and are often used as finite tables. However, the domain of a map may be infinite. \begin{supertabular}{@ {} l @ {~::~} l @ {}} \<^const>\Map.empty\ & \<^typeof>\Map.empty\\\ \<^const>\Map.map_add\ & \<^typeof>\Map.map_add\\\ \<^const>\Map.map_comp\ & \<^typeof>\Map.map_comp\\\ \<^const>\Map.restrict_map\ & @{term_type_only Map.restrict_map "('a\'b option)\'a set\('a\'b option)"}\\ \<^const>\Map.dom\ & @{term_type_only Map.dom "('a\'b option)\'a set"}\\ \<^const>\Map.ran\ & @{term_type_only Map.ran "('a\'b option)\'b set"}\\ \<^const>\Map.map_le\ & \<^typeof>\Map.map_le\\\ \<^const>\Map.map_of\ & \<^typeof>\Map.map_of\\\ \<^const>\Map.map_upds\ & \<^typeof>\Map.map_upds\\\ \end{supertabular} \subsubsection*{Syntax} \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} \<^term>\Map.empty\ & \<^term>\\x. None\\\ \<^term>\m(x:=Some y)\ & @{term[source]"m(x:=Some y)"}\\ \m(x\<^sub>1\y\<^sub>1,\,x\<^sub>n\y\<^sub>n)\ & @{text[source]"m(x\<^sub>1\y\<^sub>1)\(x\<^sub>n\y\<^sub>n)"}\\ \[x\<^sub>1\y\<^sub>1,\,x\<^sub>n\y\<^sub>n]\ & @{text[source]"Map.empty(x\<^sub>1\y\<^sub>1,\,x\<^sub>n\y\<^sub>n)"}\\ \<^term>\map_upds m xs ys\ & @{term[source]"map_upds m xs ys"}\\ \end{tabular} \section*{Infix operators in Main} % \<^theory>\Main\ \begin{center} \begin{tabular}{llll} & Operator & precedence & associativity \\ \hline Meta-logic & \\\ & 1 & right \\ & \\\ & 2 \\ \hline Logic & \\\ & 35 & right \\ &\\\ & 30 & right \\ &\\\, \\\ & 25 & right\\ &\=\, \\\ & 50 & left\\ \hline Orderings & \\\, \<\, \\\, \>\ & 50 \\ \hline Sets & \\\, \\\, \\\, \\\ & 50 \\ &\\\, \\\ & 50 \\ &\\\ & 70 & left \\ &\\\ & 65 & left \\ \hline Functions and Relations & \\\ & 55 & left\\ &\`\ & 90 & right\\ &\O\ & 75 & right\\ &\``\ & 90 & right\\ &\^^\ & 80 & right\\ \hline Numbers & \+\, \-\ & 65 & left \\ &\*\, \/\ & 70 & left \\ &\div\, \mod\ & 70 & left\\ &\^\ & 80 & right\\ &\dvd\ & 50 \\ \hline Lists & \#\, \@\ & 65 & right\\ &\!\ & 100 & left \end{tabular} \end{center} \ (*<*) end (*>*) diff --git a/src/Doc/Prog_Prove/LaTeXsugar.thy b/src/Doc/Prog_Prove/LaTeXsugar.thy --- a/src/Doc/Prog_Prove/LaTeXsugar.thy +++ b/src/Doc/Prog_Prove/LaTeXsugar.thy @@ -1,56 +1,57 @@ (* Title: HOL/Library/LaTeXsugar.thy Author: Gerwin Klein, Tobias Nipkow, Norbert Schirmer Copyright 2005 NICTA and TUM *) (*<*) theory LaTeXsugar imports Main begin (* DUMMY *) consts DUMMY :: 'a ("\<^latex>\\\_\") (* THEOREMS *) notation (Rule output) Pure.imp ("\<^latex>\\\mbox{}\\inferrule{\\mbox{\_\<^latex>\}}\\<^latex>\{\\mbox{\_\<^latex>\}}\") syntax (Rule output) "_bigimpl" :: "asms \ prop \ prop" ("\<^latex>\\\mbox{}\\inferrule{\_\<^latex>\}\\<^latex>\{\\mbox{\_\<^latex>\}}\") "_asms" :: "prop \ asms \ asms" ("\<^latex>\\\mbox{\_\<^latex>\}\\\\\/ _") "_asm" :: "prop \ asms" ("\<^latex>\\\mbox{\_\<^latex>\}\") notation (Axiom output) "Trueprop" ("\<^latex>\\\mbox{}\\inferrule{\\mbox{}}{\\mbox{\_\<^latex>\}}\") notation (IfThen output) Pure.imp ("\<^latex>\{\\normalsize{}\If\<^latex>\\\,}\ _/ \<^latex>\{\\normalsize \\,\then\<^latex>\\\,}\/ _.") syntax (IfThen output) "_bigimpl" :: "asms \ prop \ prop" ("\<^latex>\{\\normalsize{}\If\<^latex>\\\,}\ _ /\<^latex>\{\\normalsize \\,\then\<^latex>\\\,}\/ _.") "_asms" :: "prop \ asms \ asms" ("\<^latex>\\\mbox{\_\<^latex>\}\ /\<^latex>\{\\normalsize \\,\and\<^latex>\\\,}\/ _") "_asm" :: "prop \ asms" ("\<^latex>\\\mbox{\_\<^latex>\}\") notation (IfThenNoBox output) Pure.imp ("\<^latex>\{\\normalsize{}\If\<^latex>\\\,}\ _/ \<^latex>\{\\normalsize \\,\then\<^latex>\\\,}\/ _.") syntax (IfThenNoBox output) "_bigimpl" :: "asms \ prop \ prop" ("\<^latex>\{\\normalsize{}\If\<^latex>\\\,}\ _ /\<^latex>\{\\normalsize \\,\then\<^latex>\\\,}\/ _.") "_asms" :: "prop \ asms \ asms" ("_ /\<^latex>\{\\normalsize \\,\and\<^latex>\\\,}\/ _") "_asm" :: "prop \ asms" ("_") setup \ - Thy_Output.antiquotation_pretty_source \<^binding>\const_typ\ (Scan.lift Args.embedded_inner_syntax) + Document_Output.antiquotation_pretty_source \<^binding>\const_typ\ + (Scan.lift Args.embedded_inner_syntax) (fn ctxt => fn c => let val tc = Proof_Context.read_const {proper = false, strict = false} ctxt c in - Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::", + Pretty.block [Document_Output.pretty_term ctxt tc, Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)] end) \ end (*>*) diff --git a/src/Doc/antiquote_setup.ML b/src/Doc/antiquote_setup.ML --- a/src/Doc/antiquote_setup.ML +++ b/src/Doc/antiquote_setup.ML @@ -1,242 +1,242 @@ (* Title: Doc/antiquote_setup.ML Author: Makarius Auxiliary antiquotations for the Isabelle manuals. *) structure Antiquote_Setup: sig end = struct (* misc utils *) fun translate f = Symbol.explode #> map f #> implode; val clean_string = translate (fn "_" => "\\_" | "#" => "\\#" | "$" => "\\$" | "%" => "\\%" | "<" => "$<$" | ">" => "$>$" | "{" => "\\{" | "|" => "$\\mid$" | "}" => "\\}" | "\" => "-" | c => c); fun clean_name "\" = "dots" | clean_name ".." = "ddot" | clean_name "." = "dot" | clean_name "_" = "underscore" | clean_name "{" = "braceleft" | clean_name "}" = "braceright" | clean_name s = s |> translate (fn "_" => "-" | "\" => "-" | c => c); (* ML text *) local fun ml_val (toks1, []) = ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read ");" | ml_val (toks1, toks2) = ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read ");"; fun ml_op (toks1, []) = ML_Lex.read "fn _ => (op " @ toks1 @ ML_Lex.read ");" | ml_op (toks1, toks2) = ML_Lex.read "fn _ => (op " @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read ");"; fun ml_type (toks1, []) = ML_Lex.read "val _ = NONE : (" @ toks1 @ ML_Lex.read ") option;" | ml_type (toks1, toks2) = ML_Lex.read "val _ = [NONE : (" @ toks1 @ ML_Lex.read ") option, NONE : (" @ toks2 @ ML_Lex.read ") option];"; fun ml_exception (toks1, []) = ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : exn);" | ml_exception (toks1, toks2) = ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read " -> exn);"; fun ml_structure (toks, _) = ML_Lex.read "functor XXX() = struct structure XX = " @ toks @ ML_Lex.read " end;"; fun ml_functor (Antiquote.Text tok :: _, _) = ML_Lex.read "ML_Env.check_functor " @ ML_Lex.read (ML_Syntax.print_string (ML_Lex.content_of tok)) | ml_functor _ = raise Fail "Bad ML functor specification"; val is_name = ML_Lex.kind_of #> (fn kind => kind = ML_Lex.Ident orelse kind = ML_Lex.Long_Ident); fun ml_name txt = (case filter is_name (ML_Lex.tokenize txt) of toks as [_] => ML_Lex.flatten toks | _ => error ("Single ML name expected in input: " ^ quote txt)); fun prep_ml source = (#1 (Input.source_content source), ML_Lex.read_source source); -fun index_ml name kind ml = Thy_Output.antiquotation_raw name +fun index_ml name kind ml = Document_Output.antiquotation_raw name (Scan.lift (Args.text_input -- Scan.option (Args.colon |-- Args.text_input))) (fn ctxt => fn (source1, opt_source2) => let val (txt1, ants1) = prep_ml source1; val (txt2, ants2) = (case opt_source2 of SOME source => prep_ml source | NONE => ("", [])); val txt = if txt2 = "" then txt1 else if kind = "type" then txt1 ^ " = " ^ txt2 else if kind = "exception" then txt1 ^ " of " ^ txt2 else if Symbol_Pos.is_identifier (Long_Name.base_name (ml_name txt1)) then txt1 ^ ": " ^ txt2 else txt1 ^ " : " ^ txt2; val txt' = if kind = "" then txt else kind ^ " " ^ txt; val pos = Input.pos_of source1; val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags pos (ml (ants1, ants2)) handle ERROR msg => error (msg ^ Position.here pos); val kind' = if kind = "" then "ML" else "ML " ^ kind; in Latex.block [Latex.string ("\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}"), - Thy_Output.verbatim ctxt txt'] + Document_Output.verbatim ctxt txt'] end); in val _ = Theory.setup (index_ml \<^binding>\index_ML\ "" ml_val #> index_ml \<^binding>\index_ML_op\ "infix" ml_op #> index_ml \<^binding>\index_ML_type\ "type" ml_type #> index_ml \<^binding>\index_ML_exception\ "exception" ml_exception #> index_ml \<^binding>\index_ML_structure\ "structure" ml_structure #> index_ml \<^binding>\index_ML_functor\ "functor" ml_functor); end; (* named theorems *) val _ = - Theory.setup (Thy_Output.antiquotation_raw \<^binding>\named_thms\ + Theory.setup (Document_Output.antiquotation_raw \<^binding>\named_thms\ (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name))) (fn ctxt => map (fn (thm, name) => Output.output (Document_Antiquotation.format ctxt - (Document_Antiquotation.delimit ctxt (Thy_Output.pretty_thm ctxt thm))) ^ + (Document_Antiquotation.delimit ctxt (Document_Output.pretty_thm ctxt thm))) ^ enclose "\\rulename{" "}" (Output.output name)) #> space_implode "\\par\\smallskip%\n" #> Latex.string #> single - #> Thy_Output.isabelle ctxt)); + #> Document_Output.isabelle ctxt)); (* Isabelle/Isar entities (with index) *) local fun no_check (_: Proof.context) (name, _: Position.T) = name; fun check_keyword ctxt (name, pos) = if Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name then name else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos); fun check_system_option ctxt arg = (Completion.check_option (Options.default ()) ctxt arg; true) handle ERROR _ => false; val arg = enclose "{" "}" o clean_string; fun entity check markup binding index = - Thy_Output.antiquotation_raw + Document_Output.antiquotation_raw (binding |> Binding.map_name (fn name => name ^ (case index of NONE => "" | SOME true => "_def" | SOME false => "_ref"))) (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name_position)) (fn ctxt => fn (logic, (name, pos)) => let val kind = translate (fn "_" => " " | c => c) (Binding.name_of binding); val hyper_name = "{" ^ Long_Name.append kind (Long_Name.append logic (clean_name name)) ^ "}"; val hyper = enclose ("\\hyperlink" ^ hyper_name ^ "{") "}" #> index = SOME true ? enclose ("\\hypertarget" ^ hyper_name ^ "{") "}"; val idx = (case index of NONE => "" | SOME is_def => "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name); val _ = if Context_Position.is_reported ctxt pos then ignore (check ctxt (name, pos)) else (); val latex = idx ^ (Output.output name |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}") |> hyper o enclose "\\mbox{\\isa{" "}}"); in Latex.string latex end); fun entity_antiqs check markup kind = entity check markup kind NONE #> entity check markup kind (SOME true) #> entity check markup kind (SOME false); in val _ = Theory.setup (entity_antiqs no_check "" \<^binding>\syntax\ #> entity_antiqs Outer_Syntax.check_command "isacommand" \<^binding>\command\ #> entity_antiqs check_keyword "isakeyword" \<^binding>\keyword\ #> entity_antiqs check_keyword "isakeyword" \<^binding>\element\ #> entity_antiqs Method.check_name "" \<^binding>\method\ #> entity_antiqs Attrib.check_name "" \<^binding>\attribute\ #> entity_antiqs no_check "" \<^binding>\fact\ #> entity_antiqs no_check "" \<^binding>\variable\ #> entity_antiqs no_check "" \<^binding>\case\ #> entity_antiqs Document_Antiquotation.check "" \<^binding>\antiquotation\ #> entity_antiqs Document_Antiquotation.check_option "" \<^binding>\antiquotation_option\ #> entity_antiqs Document_Marker.check "" \<^binding>\document_marker\ #> entity_antiqs no_check "isasystem" \<^binding>\setting\ #> entity_antiqs check_system_option "isasystem" \<^binding>\system_option\ #> entity_antiqs no_check "" \<^binding>\inference\ #> entity_antiqs no_check "isasystem" \<^binding>\executable\ #> entity_antiqs Isabelle_Tool.check "isatool" \<^binding>\tool\ #> entity_antiqs ML_Context.check_antiquotation "" \<^binding>\ML_antiquotation\ #> entity_antiqs (K JEdit.check_action) "isasystem" \<^binding>\action\); end; (* show symbols *) val _ = - Theory.setup (Thy_Output.antiquotation_raw \<^binding>\show_symbols\ (Scan.succeed ()) + Theory.setup (Document_Output.antiquotation_raw \<^binding>\show_symbols\ (Scan.succeed ()) (fn _ => fn _ => let val symbol_name = unprefix "\\newcommand{\\isasym" #> raw_explode #> take_prefix Symbol.is_ascii_letter #> implode; val symbols = File.read \<^file>\~~/lib/texinputs/isabellesym.sty\ |> split_lines |> map_filter (fn line => (case try symbol_name line of NONE => NONE | SOME "" => NONE | SOME name => SOME ("\\verb,\\" ^ "<" ^ name ^ ">, & {\\isasym" ^ name ^ "}"))); val eol = "\\\\\n"; fun table (a :: b :: rest) = a ^ " & " ^ b ^ eol :: table rest | table [a] = [a ^ eol] | table [] = []; in Latex.string ("\\begin{supertabular}{ll@{\\qquad}ll}\n" ^ implode (table symbols) ^ "\\end{supertabular}\n") end)) end; diff --git a/src/Doc/more_antiquote.ML b/src/Doc/more_antiquote.ML --- a/src/Doc/more_antiquote.ML +++ b/src/Doc/more_antiquote.ML @@ -1,38 +1,38 @@ (* Title: Doc/more_antiquote.ML Author: Florian Haftmann, TU Muenchen More antiquotations (partly depending on Isabelle/HOL). *) structure More_Antiquote : sig end = struct (* class specifications *) val _ = - Theory.setup (Thy_Output.antiquotation_pretty \<^binding>\class_spec\ (Scan.lift Args.name) + Theory.setup (Document_Output.antiquotation_pretty \<^binding>\class_spec\ (Scan.lift Args.name) (fn ctxt => fn s => let val thy = Proof_Context.theory_of ctxt; val class = Sign.intern_class thy s; in Pretty.chunks (Class.pretty_specification thy class) end)); (* code theorem antiquotation *) val _ = - Theory.setup (Thy_Output.antiquotation_pretty \<^binding>\code_thms\ Args.term + Theory.setup (Document_Output.antiquotation_pretty \<^binding>\code_thms\ Args.term (fn ctxt => fn raw_const => let val thy = Proof_Context.theory_of ctxt; val const = Code.check_const thy raw_const; val { eqngr, ... } = Code_Preproc.obtain true { ctxt = ctxt, consts = [const], terms = [] }; val thms = Code_Preproc.cert eqngr const |> Code.equations_of_cert thy |> snd |> these |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE) |> map (HOLogic.mk_obj_eq o Variable.import_vars ctxt o Axclass.overload ctxt); - in Pretty.chunks (map (Thy_Output.pretty_thm ctxt) thms) end)); + in Pretty.chunks (map (Document_Output.pretty_thm ctxt) thms) end)); end; diff --git a/src/HOL/Library/LaTeXsugar.thy b/src/HOL/Library/LaTeXsugar.thy --- a/src/HOL/Library/LaTeXsugar.thy +++ b/src/HOL/Library/LaTeXsugar.thy @@ -1,152 +1,152 @@ (* Title: HOL/Library/LaTeXsugar.thy Author: Gerwin Klein, Tobias Nipkow, Norbert Schirmer Copyright 2005 NICTA and TUM *) (*<*) theory LaTeXsugar imports Main begin (* LOGIC *) notation (latex output) If ("(\<^latex>\\\textsf{\if\<^latex>\}\ (_)/ \<^latex>\\\textsf{\then\<^latex>\}\ (_)/ \<^latex>\\\textsf{\else\<^latex>\}\ (_))" 10) syntax (latex output) "_Let" :: "[letbinds, 'a] => 'a" ("(\<^latex>\\\textsf{\let\<^latex>\}\ (_)/ \<^latex>\\\textsf{\in\<^latex>\}\ (_))" 10) "_case_syntax":: "['a, cases_syn] => 'b" ("(\<^latex>\\\textsf{\case\<^latex>\}\ _ \<^latex>\\\textsf{\of\<^latex>\}\/ _)" 10) (* SETS *) (* empty set *) notation (latex) "Set.empty" ("\") (* insert *) translations "{x} \ A" <= "CONST insert x A" "{x,y}" <= "{x} \ {y}" "{x,y} \ A" <= "{x} \ ({y} \ A)" "{x}" <= "{x} \ \" (* set comprehension *) syntax (latex output) "_Collect" :: "pttrn => bool => 'a set" ("(1{_ | _})") "_CollectIn" :: "pttrn => 'a set => bool => 'a set" ("(1{_ \ _ | _})") translations "_Collect p P" <= "{p. P}" "_Collect p P" <= "{p|xs. P}" "_CollectIn p A P" <= "{p : A. P}" (* card *) notation (latex output) card ("|_|") (* LISTS *) (* Cons *) notation (latex) Cons ("_ \/ _" [66,65] 65) (* length *) notation (latex output) length ("|_|") (* nth *) notation (latex output) nth ("_\<^latex>\\\ensuremath{_{[\\mathit{\_\<^latex>\}]}}\" [1000,0] 1000) (* DUMMY *) consts DUMMY :: 'a ("\<^latex>\\\_\") (* THEOREMS *) notation (Rule output) Pure.imp ("\<^latex>\\\mbox{}\\inferrule{\\mbox{\_\<^latex>\}}\\<^latex>\{\\mbox{\_\<^latex>\}}\") syntax (Rule output) "_bigimpl" :: "asms \ prop \ prop" ("\<^latex>\\\mbox{}\\inferrule{\_\<^latex>\}\\<^latex>\{\\mbox{\_\<^latex>\}}\") "_asms" :: "prop \ asms \ asms" ("\<^latex>\\\mbox{\_\<^latex>\}\\\\\/ _") "_asm" :: "prop \ asms" ("\<^latex>\\\mbox{\_\<^latex>\}\") notation (Axiom output) "Trueprop" ("\<^latex>\\\mbox{}\\inferrule{\\mbox{}}{\\mbox{\_\<^latex>\}}\") notation (IfThen output) Pure.imp ("\<^latex>\{\\normalsize{}\If\<^latex>\\\,}\ _/ \<^latex>\{\\normalsize \\,\then\<^latex>\\\,}\/ _.") syntax (IfThen output) "_bigimpl" :: "asms \ prop \ prop" ("\<^latex>\{\\normalsize{}\If\<^latex>\\\,}\ _ /\<^latex>\{\\normalsize \\,\then\<^latex>\\\,}\/ _.") "_asms" :: "prop \ asms \ asms" ("\<^latex>\\\mbox{\_\<^latex>\}\ /\<^latex>\{\\normalsize \\,\and\<^latex>\\\,}\/ _") "_asm" :: "prop \ asms" ("\<^latex>\\\mbox{\_\<^latex>\}\") notation (IfThenNoBox output) Pure.imp ("\<^latex>\{\\normalsize{}\If\<^latex>\\\,}\ _/ \<^latex>\{\\normalsize \\,\then\<^latex>\\\,}\/ _.") syntax (IfThenNoBox output) "_bigimpl" :: "asms \ prop \ prop" ("\<^latex>\{\\normalsize{}\If\<^latex>\\\,}\ _ /\<^latex>\{\\normalsize \\,\then\<^latex>\\\,}\/ _.") "_asms" :: "prop \ asms \ asms" ("_ /\<^latex>\{\\normalsize \\,\and\<^latex>\\\,}\/ _") "_asm" :: "prop \ asms" ("_") setup \ - Thy_Output.antiquotation_pretty_source_embedded \<^binding>\const_typ\ + Document_Output.antiquotation_pretty_source_embedded \<^binding>\const_typ\ (Scan.lift Args.embedded_inner_syntax) (fn ctxt => fn c => let val tc = Proof_Context.read_const {proper = false, strict = false} ctxt c in - Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::", + Pretty.block [Document_Output.pretty_term ctxt tc, Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)] end) \ setup\ let fun dummy_pats (wrap $ (eq $ lhs $ rhs)) = let val rhs_vars = Term.add_vars rhs []; fun dummy (v as Var (ixn as (_, T))) = if member ((=) ) rhs_vars ixn then v else Const (\<^const_name>\DUMMY\, T) | dummy (t $ u) = dummy t $ dummy u | dummy (Abs (n, T, b)) = Abs (n, T, dummy b) | dummy t = t; in wrap $ (eq $ dummy lhs $ rhs) end in Term_Style.setup \<^binding>\dummy_pats\ (Scan.succeed (K dummy_pats)) end \ setup \ let fun eta_expand Ts t xs = case t of Abs(x,T,t) => let val (t', xs') = eta_expand (T::Ts) t xs in (Abs (x, T, t'), xs') end | _ => let val (a,ts) = strip_comb t (* assume a atomic *) val (ts',xs') = fold_map (eta_expand Ts) ts xs val t' = list_comb (a, ts'); val Bs = binder_types (fastype_of1 (Ts,t)); val n = Int.min (length Bs, length xs'); val bs = map Bound ((n - 1) downto 0); val xBs = ListPair.zip (xs',Bs); val xs'' = drop n xs'; val t'' = fold_rev Term.abs xBs (list_comb(t', bs)) in (t'', xs'') end val style_eta_expand = (Scan.repeat Args.name) >> (fn xs => fn ctxt => fn t => fst (eta_expand [] t xs)) in Term_Style.setup \<^binding>\eta_expand\ style_eta_expand end \ end (*>*) diff --git a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML @@ -1,1270 +1,1270 @@ (* Title: HOL/Tools/Ctr_Sugar/ctr_sugar.ML Author: Jasmin Blanchette, TU Muenchen Author: Martin Desharnais, TU Muenchen Copyright 2012, 2013 Wrapping existing freely generated type's constructors. *) signature CTR_SUGAR = sig datatype ctr_sugar_kind = Datatype | Codatatype | Record | Unknown type ctr_sugar = {kind: ctr_sugar_kind, T: typ, ctrs: term list, casex: term, discs: term list, selss: term list list, exhaust: thm, nchotomy: thm, injects: thm list, distincts: thm list, case_thms: thm list, case_cong: thm, case_cong_weak: thm, case_distribs: thm list, split: thm, split_asm: thm, disc_defs: thm list, disc_thmss: thm list list, discIs: thm list, disc_eq_cases: thm list, sel_defs: thm list, sel_thmss: thm list list, distinct_discsss: thm list list list, exhaust_discs: thm list, exhaust_sels: thm list, collapses: thm list, expands: thm list, split_sels: thm list, split_sel_asms: thm list, case_eq_ifs: thm list}; val morph_ctr_sugar: morphism -> ctr_sugar -> ctr_sugar val transfer_ctr_sugar: theory -> ctr_sugar -> ctr_sugar val ctr_sugar_of: Proof.context -> string -> ctr_sugar option val ctr_sugar_of_global: theory -> string -> ctr_sugar option val ctr_sugars_of: Proof.context -> ctr_sugar list val ctr_sugars_of_global: theory -> ctr_sugar list val ctr_sugar_of_case: Proof.context -> string -> ctr_sugar option val ctr_sugar_of_case_global: theory -> string -> ctr_sugar option val ctr_sugar_interpretation: string -> (ctr_sugar -> local_theory -> local_theory) -> theory -> theory val interpret_ctr_sugar: (string -> bool) -> ctr_sugar -> local_theory -> local_theory val register_ctr_sugar_raw: ctr_sugar -> local_theory -> local_theory val register_ctr_sugar: (string -> bool) -> ctr_sugar -> local_theory -> local_theory val default_register_ctr_sugar_global: (string -> bool) -> ctr_sugar -> theory -> theory val mk_half_pairss: 'a list * 'a list -> ('a * 'a) list list val join_halves: int -> 'a list list -> 'a list list -> 'a list * 'a list list list val mk_ctr: typ list -> term -> term val mk_case: typ list -> typ -> term -> term val mk_disc_or_sel: typ list -> term -> term val name_of_ctr: term -> string val name_of_disc: term -> string val dest_ctr: Proof.context -> string -> term -> term * term list val dest_case: Proof.context -> string -> typ list -> term -> (ctr_sugar * term list * term list) option type ('c, 'a) ctr_spec = (binding * 'c) * 'a list val disc_of_ctr_spec: ('c, 'a) ctr_spec -> binding val ctr_of_ctr_spec: ('c, 'a) ctr_spec -> 'c val args_of_ctr_spec: ('c, 'a) ctr_spec -> 'a list val code_plugin: string type ctr_options = (string -> bool) * bool type ctr_options_cmd = (Proof.context -> string -> bool) * bool val fake_local_theory_for_sel_defaults: (binding * typ) list -> Proof.context -> Proof.context val free_constructors: ctr_sugar_kind -> ({prems: thm list, context: Proof.context} -> tactic) list list -> ((ctr_options * binding) * (term, binding) ctr_spec list) * term list -> local_theory -> ctr_sugar * local_theory val free_constructors_cmd: ctr_sugar_kind -> ((((Proof.context -> Plugin_Name.filter) * bool) * binding) * ((binding * string) * binding list) list) * string list -> Proof.context -> Proof.state val default_ctr_options: ctr_options val default_ctr_options_cmd: ctr_options_cmd val parse_bound_term: (binding * string) parser val parse_ctr_options: ctr_options_cmd parser val parse_ctr_spec: 'c parser -> 'a parser -> ('c, 'a) ctr_spec parser val parse_sel_default_eqs: string list parser end; structure Ctr_Sugar : CTR_SUGAR = struct open Ctr_Sugar_Util open Ctr_Sugar_Tactics open Ctr_Sugar_Code datatype ctr_sugar_kind = Datatype | Codatatype | Record | Unknown; type ctr_sugar = {kind: ctr_sugar_kind, T: typ, ctrs: term list, casex: term, discs: term list, selss: term list list, exhaust: thm, nchotomy: thm, injects: thm list, distincts: thm list, case_thms: thm list, case_cong: thm, case_cong_weak: thm, case_distribs: thm list, split: thm, split_asm: thm, disc_defs: thm list, disc_thmss: thm list list, discIs: thm list, disc_eq_cases: thm list, sel_defs: thm list, sel_thmss: thm list list, distinct_discsss: thm list list list, exhaust_discs: thm list, exhaust_sels: thm list, collapses: thm list, expands: thm list, split_sels: thm list, split_sel_asms: thm list, case_eq_ifs: thm list}; fun morph_ctr_sugar phi ({kind, T, ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts, case_thms, case_cong, case_cong_weak, case_distribs, split, split_asm, disc_defs, disc_thmss, discIs, disc_eq_cases, sel_defs, sel_thmss, distinct_discsss, exhaust_discs, exhaust_sels, collapses, expands, split_sels, split_sel_asms, case_eq_ifs} : ctr_sugar) = {kind = kind, T = Morphism.typ phi T, ctrs = map (Morphism.term phi) ctrs, casex = Morphism.term phi casex, discs = map (Morphism.term phi) discs, selss = map (map (Morphism.term phi)) selss, exhaust = Morphism.thm phi exhaust, nchotomy = Morphism.thm phi nchotomy, injects = map (Morphism.thm phi) injects, distincts = map (Morphism.thm phi) distincts, case_thms = map (Morphism.thm phi) case_thms, case_cong = Morphism.thm phi case_cong, case_cong_weak = Morphism.thm phi case_cong_weak, case_distribs = map (Morphism.thm phi) case_distribs, split = Morphism.thm phi split, split_asm = Morphism.thm phi split_asm, disc_defs = map (Morphism.thm phi) disc_defs, disc_thmss = map (map (Morphism.thm phi)) disc_thmss, discIs = map (Morphism.thm phi) discIs, disc_eq_cases = map (Morphism.thm phi) disc_eq_cases, sel_defs = map (Morphism.thm phi) sel_defs, sel_thmss = map (map (Morphism.thm phi)) sel_thmss, distinct_discsss = map (map (map (Morphism.thm phi))) distinct_discsss, exhaust_discs = map (Morphism.thm phi) exhaust_discs, exhaust_sels = map (Morphism.thm phi) exhaust_sels, collapses = map (Morphism.thm phi) collapses, expands = map (Morphism.thm phi) expands, split_sels = map (Morphism.thm phi) split_sels, split_sel_asms = map (Morphism.thm phi) split_sel_asms, case_eq_ifs = map (Morphism.thm phi) case_eq_ifs}; val transfer_ctr_sugar = morph_ctr_sugar o Morphism.transfer_morphism; structure Data = Generic_Data ( type T = (Position.T * ctr_sugar) Symtab.table; val empty = Symtab.empty; val extend = I; fun merge data : T = Symtab.merge (K true) data; ); fun ctr_sugar_of_generic context = Option.map (transfer_ctr_sugar (Context.theory_of context) o #2) o Symtab.lookup (Data.get context); fun ctr_sugars_of_generic context = Symtab.fold (cons o transfer_ctr_sugar (Context.theory_of context) o #2 o #2) (Data.get context) []; fun ctr_sugar_of_case_generic context s = find_first (fn {casex = Const (s', _), ...} => s' = s | _ => false) (ctr_sugars_of_generic context); val ctr_sugar_of = ctr_sugar_of_generic o Context.Proof; val ctr_sugar_of_global = ctr_sugar_of_generic o Context.Theory; val ctr_sugars_of = ctr_sugars_of_generic o Context.Proof; val ctr_sugars_of_global = ctr_sugars_of_generic o Context.Theory; val ctr_sugar_of_case = ctr_sugar_of_case_generic o Context.Proof; val ctr_sugar_of_case_global = ctr_sugar_of_case_generic o Context.Theory; structure Ctr_Sugar_Plugin = Plugin(type T = ctr_sugar); fun ctr_sugar_interpretation name f = Ctr_Sugar_Plugin.interpretation name (fn ctr_sugar => fn lthy => f (transfer_ctr_sugar (Proof_Context.theory_of lthy) ctr_sugar) lthy); val interpret_ctr_sugar = Ctr_Sugar_Plugin.data; fun register_ctr_sugar_raw (ctr_sugar as {T = Type (name, _), ...}) = Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => fn context => let val pos = Position.thread_data () in Data.map (Symtab.update (name, (pos, morph_ctr_sugar phi ctr_sugar))) context end); fun register_ctr_sugar plugins ctr_sugar = register_ctr_sugar_raw ctr_sugar #> interpret_ctr_sugar plugins ctr_sugar; fun default_register_ctr_sugar_global plugins (ctr_sugar as {T = Type (name, _), ...}) thy = let val tab = Data.get (Context.Theory thy); val pos = Position.thread_data (); in if Symtab.defined tab name then thy else thy |> Context.theory_map (Data.put (Symtab.update_new (name, (pos, ctr_sugar)) tab)) |> Named_Target.theory_map (Ctr_Sugar_Plugin.data plugins ctr_sugar) end; val is_prefix = "is_"; val un_prefix = "un_"; val not_prefix = "not_"; fun mk_unN 1 1 suf = un_prefix ^ suf | mk_unN _ l suf = un_prefix ^ suf ^ string_of_int l; val caseN = "case"; val case_congN = "case_cong"; val case_eq_ifN = "case_eq_if"; val collapseN = "collapse"; val discN = "disc"; val disc_eq_caseN = "disc_eq_case"; val discIN = "discI"; val distinctN = "distinct"; val distinct_discN = "distinct_disc"; val exhaustN = "exhaust"; val exhaust_discN = "exhaust_disc"; val expandN = "expand"; val injectN = "inject"; val nchotomyN = "nchotomy"; val selN = "sel"; val exhaust_selN = "exhaust_sel"; val splitN = "split"; val split_asmN = "split_asm"; val split_selN = "split_sel"; val split_sel_asmN = "split_sel_asm"; val splitsN = "splits"; val split_selsN = "split_sels"; val case_cong_weak_thmsN = "case_cong_weak"; val case_distribN = "case_distrib"; val cong_attrs = @{attributes [cong]}; val dest_attrs = @{attributes [dest]}; val safe_elim_attrs = @{attributes [elim!]}; val iff_attrs = @{attributes [iff]}; val inductsimp_attrs = @{attributes [induct_simp]}; val nitpicksimp_attrs = @{attributes [nitpick_simp]}; val simp_attrs = @{attributes [simp]}; fun unflat_lookup eq xs ys = map (fn xs' => permute_like_unique eq xs xs' ys); fun mk_half_pairss' _ ([], []) = [] | mk_half_pairss' indent (x :: xs, _ :: ys) = indent @ fold_rev (cons o single o pair x) ys (mk_half_pairss' ([] :: indent) (xs, ys)); fun mk_half_pairss p = mk_half_pairss' [[]] p; fun join_halves n half_xss other_half_xss = (splice (flat half_xss) (flat other_half_xss), map2 (map2 append) (Library.chop_groups n half_xss) (transpose (Library.chop_groups n other_half_xss))); fun mk_undefined T = Const (\<^const_name>\undefined\, T); fun mk_ctr Ts t = let val Type (_, Ts0) = body_type (fastype_of t) in subst_nonatomic_types (Ts0 ~~ Ts) t end; fun mk_case Ts T t = let val (Type (_, Ts0), body) = strip_type (fastype_of t) |>> List.last in subst_nonatomic_types ((body, T) :: (Ts0 ~~ Ts)) t end; fun mk_disc_or_sel Ts t = subst_nonatomic_types (snd (Term.dest_Type (domain_type (fastype_of t))) ~~ Ts) t; val name_of_ctr = name_of_const "constructor" body_type; fun name_of_disc t = (case head_of t of Abs (_, _, \<^const>\Not\ $ (t' $ Bound 0)) => Long_Name.map_base_name (prefix not_prefix) (name_of_disc t') | Abs (_, _, Const (\<^const_name>\HOL.eq\, _) $ Bound 0 $ t') => Long_Name.map_base_name (prefix is_prefix) (name_of_disc t') | Abs (_, _, \<^const>\Not\ $ (Const (\<^const_name>\HOL.eq\, _) $ Bound 0 $ t')) => Long_Name.map_base_name (prefix (not_prefix ^ is_prefix)) (name_of_disc t') | t' => name_of_const "discriminator" (perhaps (try domain_type)) t'); val base_name_of_ctr = Long_Name.base_name o name_of_ctr; fun dest_ctr ctxt s t = let val (f, args) = Term.strip_comb t in (case ctr_sugar_of ctxt s of SOME {ctrs, ...} => (case find_first (can (fo_match ctxt f)) ctrs of SOME f' => (f', args) | NONE => raise Fail "dest_ctr") | NONE => raise Fail "dest_ctr") end; fun dest_case ctxt s Ts t = (case Term.strip_comb t of (Const (c, _), args as _ :: _) => (case ctr_sugar_of ctxt s of SOME (ctr_sugar as {casex = Const (case_name, _), discs = discs0, selss = selss0, ...}) => if case_name = c then let val n = length discs0 in if n < length args then let val (branches, obj :: leftovers) = chop n args; val discs = map (mk_disc_or_sel Ts) discs0; val selss = map (map (mk_disc_or_sel Ts)) selss0; val conds = map (rapp obj) discs; val branch_argss = map (fn sels => map (rapp obj) sels @ leftovers) selss; val branches' = map2 (curry Term.betapplys) branches branch_argss; in SOME (ctr_sugar, conds, branches') end else NONE end else NONE | _ => NONE) | _ => NONE); fun const_or_free_name (Const (s, _)) = Long_Name.base_name s | const_or_free_name (Free (s, _)) = s | const_or_free_name t = raise TERM ("const_or_free_name", [t]) fun extract_sel_default ctxt t = let fun malformed () = error ("Malformed selector default value equation: " ^ Syntax.string_of_term ctxt t); val ((sel, (ctr, vars)), rhs) = fst (Term.replace_dummy_patterns (Syntax.check_term ctxt t) 0) |> HOLogic.dest_eq |>> (Term.dest_comb #>> const_or_free_name ##> (Term.strip_comb #>> (Term.dest_Const #> fst))) handle TERM _ => malformed (); in if forall (is_Free orf is_Var) vars andalso not (has_duplicates (op aconv) vars) then ((ctr, sel), fold_rev Term.lambda vars rhs) else malformed () end; (* Ideally, we would enrich the context with constants rather than free variables. *) fun fake_local_theory_for_sel_defaults sel_bTs = Proof_Context.allow_dummies #> Proof_Context.add_fixes (map (fn (b, T) => (b, SOME T, NoSyn)) sel_bTs) #> snd; type ('c, 'a) ctr_spec = (binding * 'c) * 'a list; fun disc_of_ctr_spec ((disc, _), _) = disc; fun ctr_of_ctr_spec ((_, ctr), _) = ctr; fun args_of_ctr_spec (_, args) = args; val code_plugin = Plugin_Name.declare_setup \<^binding>\code\; fun prepare_free_constructors kind prep_plugins prep_term ((((raw_plugins, discs_sels), raw_case_binding), ctr_specs), sel_default_eqs) no_defs_lthy = let val plugins = prep_plugins no_defs_lthy raw_plugins; (* TODO: sanity checks on arguments *) val raw_ctrs = map ctr_of_ctr_spec ctr_specs; val raw_disc_bindings = map disc_of_ctr_spec ctr_specs; val raw_sel_bindingss = map args_of_ctr_spec ctr_specs; val n = length raw_ctrs; val ks = 1 upto n; val _ = n > 0 orelse error "No constructors specified"; val ctrs0 = map (prep_term no_defs_lthy) raw_ctrs; val (fcT_name, As0) = (case body_type (fastype_of (hd ctrs0)) of Type T' => T' | _ => error "Expected type constructor in body type of constructor"); val _ = forall ((fn Type (T_name, _) => T_name = fcT_name | _ => false) o body_type o fastype_of) (tl ctrs0) orelse error "Constructors not constructing same type"; val fc_b_name = Long_Name.base_name fcT_name; val fc_b = Binding.name fc_b_name; fun qualify mandatory = Binding.qualify mandatory fc_b_name; val (unsorted_As, [B, C]) = no_defs_lthy |> variant_tfrees (map (fst o dest_TFree_or_TVar) As0) ||> fst o mk_TFrees 2; val As = map2 (resort_tfree_or_tvar o snd o dest_TFree_or_TVar) As0 unsorted_As; val fcT = Type (fcT_name, As); val ctrs = map (mk_ctr As) ctrs0; val ctr_Tss = map (binder_types o fastype_of) ctrs; val ms = map length ctr_Tss; fun can_definitely_rely_on_disc k = not (Binding.is_empty (nth raw_disc_bindings (k - 1))) orelse nth ms (k - 1) = 0; fun can_rely_on_disc k = can_definitely_rely_on_disc k orelse (k = 1 andalso not (can_definitely_rely_on_disc 2)); fun should_omit_disc_binding k = n = 1 orelse (n = 2 andalso can_rely_on_disc (3 - k)); val equal_binding = \<^binding>\=\; fun is_disc_binding_valid b = not (Binding.is_empty b orelse Binding.eq_name (b, equal_binding)); val standard_disc_binding = Binding.name o prefix is_prefix o base_name_of_ctr; val disc_bindings = raw_disc_bindings |> @{map 4} (fn k => fn m => fn ctr => fn disc => qualify false (if Binding.is_empty disc then if m = 0 then equal_binding else if should_omit_disc_binding k then disc else standard_disc_binding ctr else if Binding.eq_name (disc, standard_binding) then standard_disc_binding ctr else disc)) ks ms ctrs0; fun standard_sel_binding m l = Binding.name o mk_unN m l o base_name_of_ctr; val sel_bindingss = @{map 3} (fn ctr => fn m => map2 (fn l => fn sel => qualify false (if Binding.is_empty sel orelse Binding.eq_name (sel, standard_binding) then standard_sel_binding m l ctr else sel)) (1 upto m) o pad_list Binding.empty m) ctrs0 ms raw_sel_bindingss; val add_bindings = Variable.add_fixes (distinct (op =) (filter Symbol_Pos.is_identifier (map Binding.name_of (disc_bindings @ flat sel_bindingss)))) #> snd; val case_Ts = map (fn Ts => Ts ---> B) ctr_Tss; val (((((((((u, exh_y), xss), yss), fs), gs), w), (p, p'))), _) = no_defs_lthy |> add_bindings |> yield_singleton (mk_Frees fc_b_name) fcT ||>> yield_singleton (mk_Frees "y") fcT (* for compatibility with "datatype_realizer.ML" *) ||>> mk_Freess "x" ctr_Tss ||>> mk_Freess "y" ctr_Tss ||>> mk_Frees "f" case_Ts ||>> mk_Frees "g" case_Ts ||>> yield_singleton (mk_Frees "z") B ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT; val q = Free (fst p', mk_pred1T B); val xctrs = map2 (curry Term.list_comb) ctrs xss; val yctrs = map2 (curry Term.list_comb) ctrs yss; val xfs = map2 (curry Term.list_comb) fs xss; val xgs = map2 (curry Term.list_comb) gs xss; (* TODO: Eta-expension is for compatibility with the old datatype package (but it also provides nicer names). Consider removing. *) val eta_fs = map2 (fold_rev Term.lambda) xss xfs; val eta_gs = map2 (fold_rev Term.lambda) xss xgs; val case_binding = qualify false (if Binding.is_empty raw_case_binding orelse Binding.eq_name (raw_case_binding, standard_binding) then Binding.prefix_name (caseN ^ "_") fc_b else raw_case_binding); fun mk_case_disj xctr xf xs = list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (u, xctr), HOLogic.mk_eq (w, xf))); val case_rhs = fold_rev (fold_rev Term.lambda) [fs, [u]] (Const (\<^const_name>\The\, (B --> HOLogic.boolT) --> B) $ Term.lambda w (Library.foldr1 HOLogic.mk_disj (@{map 3} mk_case_disj xctrs xfs xss))); val ((raw_case, (_, raw_case_def)), (lthy, lthy_old)) = no_defs_lthy |> (snd o Local_Theory.begin_nested) |> Local_Theory.define ((case_binding, NoSyn), ((Binding.concealed (Thm.def_binding case_binding), []), case_rhs)) ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy_old lthy; val case_def = Morphism.thm phi raw_case_def; val case0 = Morphism.term phi raw_case; val casex = mk_case As B case0; val casexC = mk_case As C case0; val casexBool = mk_case As HOLogic.boolT case0; fun mk_uu_eq () = HOLogic.mk_eq (u, u); val exist_xs_u_eq_ctrs = map2 (fn xctr => fn xs => list_exists_free xs (HOLogic.mk_eq (u, xctr))) xctrs xss; val unique_disc_no_def = TrueI; (*arbitrary marker*) val alternate_disc_no_def = FalseE; (*arbitrary marker*) fun alternate_disc_lhs get_udisc k = HOLogic.mk_not (let val b = nth disc_bindings (k - 1) in if is_disc_binding_valid b then get_udisc b (k - 1) else nth exist_xs_u_eq_ctrs (k - 1) end); val no_discs_sels = not discs_sels andalso forall (forall Binding.is_empty) (raw_disc_bindings :: raw_sel_bindingss) andalso null sel_default_eqs; val (all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy) = if no_discs_sels then (true, [], [], [], [], [], lthy) else let val all_sel_bindings = flat sel_bindingss; val num_all_sel_bindings = length all_sel_bindings; val uniq_sel_bindings = distinct Binding.eq_name all_sel_bindings; val all_sels_distinct = (length uniq_sel_bindings = num_all_sel_bindings); val sel_binding_index = if all_sels_distinct then 1 upto num_all_sel_bindings else map (fn b => find_index (curry Binding.eq_name b) uniq_sel_bindings) all_sel_bindings; val all_proto_sels = flat (@{map 3} (fn k => fn xs => map (pair k o pair xs)) ks xss xss); val sel_infos = AList.group (op =) (sel_binding_index ~~ all_proto_sels) |> sort (int_ord o apply2 fst) |> map snd |> curry (op ~~) uniq_sel_bindings; val sel_bindings = map fst sel_infos; val sel_defaults = if null sel_default_eqs then [] else let val sel_Ts = map (curry (op -->) fcT o fastype_of o snd o snd o hd o snd) sel_infos; val fake_lthy = fake_local_theory_for_sel_defaults (sel_bindings ~~ sel_Ts) no_defs_lthy; in map (extract_sel_default fake_lthy o prep_term fake_lthy) sel_default_eqs end; fun disc_free b = Free (Binding.name_of b, mk_pred1T fcT); fun disc_spec b exist_xs_u_eq_ctr = mk_Trueprop_eq (disc_free b $ u, exist_xs_u_eq_ctr); fun alternate_disc k = Term.lambda u (alternate_disc_lhs (K o rapp u o disc_free) (3 - k)); fun mk_sel_case_args b proto_sels T = @{map 3} (fn Const (c, _) => fn Ts => fn k => (case AList.lookup (op =) proto_sels k of NONE => (case filter (curry (op =) (c, Binding.name_of b) o fst) sel_defaults of [] => fold_rev (Term.lambda o curry Free Name.uu) Ts (mk_undefined T) | [(_, t)] => t | _ => error "Multiple default values for selector/constructor pair") | SOME (xs, x) => fold_rev Term.lambda xs x)) ctrs ctr_Tss ks; fun sel_spec b proto_sels = let val _ = (case duplicates (op =) (map fst proto_sels) of k :: _ => error ("Duplicate selector name " ^ quote (Binding.name_of b) ^ " for constructor " ^ quote (Syntax.string_of_term lthy (nth ctrs (k - 1)))) | [] => ()) val T = (case distinct (op =) (map (fastype_of o snd o snd) proto_sels) of [T] => T | T :: T' :: _ => error ("Inconsistent range type for selector " ^ quote (Binding.name_of b) ^ ": " ^ quote (Syntax.string_of_typ lthy T) ^ " vs. " ^ quote (Syntax.string_of_typ lthy T'))); in mk_Trueprop_eq (Free (Binding.name_of b, fcT --> T) $ u, Term.list_comb (mk_case As T case0, mk_sel_case_args b proto_sels T) $ u) end; fun unflat_selss xs = unflat_lookup Binding.eq_name sel_bindings xs sel_bindingss; val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) = lthy |> (snd o Local_Theory.begin_nested) |> apfst split_list o @{fold_map 3} (fn k => fn exist_xs_u_eq_ctr => fn b => if Binding.is_empty b then if n = 1 then pair (Term.lambda u (mk_uu_eq ()), unique_disc_no_def) else pair (alternate_disc k, alternate_disc_no_def) else if Binding.eq_name (b, equal_binding) then pair (Term.lambda u exist_xs_u_eq_ctr, refl) else Specification.definition (SOME (b, NONE, NoSyn)) [] [] ((Thm.def_binding b, []), disc_spec b exist_xs_u_eq_ctr) #>> apsnd snd) ks exist_xs_u_eq_ctrs disc_bindings ||>> apfst split_list o fold_map (fn (b, proto_sels) => Specification.definition (SOME (b, NONE, NoSyn)) [] [] ((Thm.def_binding b, []), sel_spec b proto_sels) #>> apsnd snd) sel_infos ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy lthy'; val disc_defs = map (Morphism.thm phi) raw_disc_defs; val sel_defs = map (Morphism.thm phi) raw_sel_defs; val sel_defss = unflat_selss sel_defs; val discs0 = map (Morphism.term phi) raw_discs; val selss0 = unflat_selss (map (Morphism.term phi) raw_sels); val discs = map (mk_disc_or_sel As) discs0; val selss = map (map (mk_disc_or_sel As)) selss0; in (all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy') end; fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p); val exhaust_goal = let fun mk_prem xctr xs = fold_rev Logic.all xs (mk_imp_p [mk_Trueprop_eq (exh_y, xctr)]) in fold_rev Logic.all [p, exh_y] (mk_imp_p (map2 mk_prem xctrs xss)) end; val inject_goalss = let fun mk_goal _ _ [] [] = [] | mk_goal xctr yctr xs ys = [fold_rev Logic.all (xs @ ys) (mk_Trueprop_eq (HOLogic.mk_eq (xctr, yctr), Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) xs ys)))]; in @{map 4} mk_goal xctrs yctrs xss yss end; val half_distinct_goalss = let fun mk_goal ((xs, xc), (xs', xc')) = fold_rev Logic.all (xs @ xs') (HOLogic.mk_Trueprop (HOLogic.mk_not (HOLogic.mk_eq (xc, xc')))); in map (map mk_goal) (mk_half_pairss (`I (xss ~~ xctrs))) end; val goalss = [exhaust_goal] :: inject_goalss @ half_distinct_goalss; fun after_qed ([exhaust_thm] :: thmss) lthy = let val ((((((((u, u'), (xss, xss')), fs), gs), h), v), p), _) = lthy |> add_bindings |> yield_singleton (apfst (op ~~) oo mk_Frees' fc_b_name) fcT ||>> mk_Freess' "x" ctr_Tss ||>> mk_Frees "f" case_Ts ||>> mk_Frees "g" case_Ts ||>> yield_singleton (mk_Frees "h") (B --> C) ||>> yield_singleton (mk_Frees (fc_b_name ^ "'")) fcT ||>> yield_singleton (mk_Frees "P") HOLogic.boolT; val xfs = map2 (curry Term.list_comb) fs xss; val xgs = map2 (curry Term.list_comb) gs xss; val fcase = Term.list_comb (casex, fs); val ufcase = fcase $ u; val vfcase = fcase $ v; val eta_fcase = Term.list_comb (casex, eta_fs); val eta_gcase = Term.list_comb (casex, eta_gs); val eta_ufcase = eta_fcase $ u; val eta_vgcase = eta_gcase $ v; fun mk_uu_eq () = HOLogic.mk_eq (u, u); val uv_eq = mk_Trueprop_eq (u, v); val ((inject_thms, inject_thmss), half_distinct_thmss) = chop n thmss |>> `flat; val rho_As = map (fn (T, U) => (dest_TVar T, Thm.ctyp_of lthy U)) (map Logic.varifyT_global As ~~ As); fun inst_thm t thm = Thm.instantiate' [] [SOME (Thm.cterm_of lthy t)] (Thm.instantiate (rho_As, []) (Drule.zero_var_indexes thm)); val uexhaust_thm = inst_thm u exhaust_thm; val exhaust_cases = map base_name_of_ctr ctrs; val other_half_distinct_thmss = map (map (fn thm => thm RS not_sym)) half_distinct_thmss; val (distinct_thms, (distinct_thmsss', distinct_thmsss)) = join_halves n half_distinct_thmss other_half_distinct_thmss ||> `transpose; val nchotomy_thm = let val goal = HOLogic.mk_Trueprop (HOLogic.mk_all (fst u', snd u', Library.foldr1 HOLogic.mk_disj exist_xs_u_eq_ctrs)); in Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => mk_nchotomy_tac ctxt n exhaust_thm) |> Thm.close_derivation \<^here> end; val case_thms = let val goals = @{map 3} (fn xctr => fn xf => fn xs => fold_rev Logic.all (fs @ xs) (mk_Trueprop_eq (fcase $ xctr, xf))) xctrs xfs xss; in @{map 4} (fn k => fn goal => fn injects => fn distinctss => Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => mk_case_tac ctxt n k case_def injects distinctss) |> Thm.close_derivation \<^here>) ks goals inject_thmss distinct_thmsss end; val (case_cong_thm, case_cong_weak_thm) = let fun mk_prem xctr xs xf xg = fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (v, xctr), mk_Trueprop_eq (xf, xg))); val goal = Logic.list_implies (uv_eq :: @{map 4} mk_prem xctrs xss xfs xgs, mk_Trueprop_eq (eta_ufcase, eta_vgcase)); val weak_goal = Logic.mk_implies (uv_eq, mk_Trueprop_eq (ufcase, vfcase)); val vars = Variable.add_free_names lthy goal []; val weak_vars = Variable.add_free_names lthy weak_goal []; in (Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_case_cong_tac ctxt uexhaust_thm case_thms), Goal.prove_sorry lthy weak_vars [] weak_goal (fn {context = ctxt, prems = _} => etac ctxt arg_cong 1)) |> apply2 (Thm.close_derivation \<^here>) end; val split_lhs = q $ ufcase; fun mk_split_conjunct xctr xs f_xs = list_all_free xs (HOLogic.mk_imp (HOLogic.mk_eq (u, xctr), q $ f_xs)); fun mk_split_disjunct xctr xs f_xs = list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (u, xctr), HOLogic.mk_not (q $ f_xs))); fun mk_split_goal xctrs xss xfs = mk_Trueprop_eq (split_lhs, Library.foldr1 HOLogic.mk_conj (@{map 3} mk_split_conjunct xctrs xss xfs)); fun mk_split_asm_goal xctrs xss xfs = mk_Trueprop_eq (split_lhs, HOLogic.mk_not (Library.foldr1 HOLogic.mk_disj (@{map 3} mk_split_disjunct xctrs xss xfs))); fun prove_split selss goal = Variable.add_free_names lthy goal [] |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_split_tac ctxt uexhaust_thm case_thms selss inject_thmss distinct_thmsss)) |> Thm.close_derivation \<^here>; fun prove_split_asm asm_goal split_thm = Variable.add_free_names lthy asm_goal [] |> (fn vars => Goal.prove_sorry lthy vars [] asm_goal (fn {context = ctxt, ...} => mk_split_asm_tac ctxt split_thm)) |> Thm.close_derivation \<^here>; val (split_thm, split_asm_thm) = let val goal = mk_split_goal xctrs xss xfs; val asm_goal = mk_split_asm_goal xctrs xss xfs; val thm = prove_split (replicate n []) goal; val asm_thm = prove_split_asm asm_goal thm; in (thm, asm_thm) end; val (sel_defs, all_sel_thms, sel_thmss, nontriv_disc_defs, disc_thmss, nontriv_disc_thmss, discI_thms, nontriv_discI_thms, distinct_disc_thms, distinct_disc_thmsss, exhaust_disc_thms, exhaust_sel_thms, all_collapse_thms, safe_collapse_thms, expand_thms, split_sel_thms, split_sel_asm_thms, case_eq_if_thms, disc_eq_case_thms) = if no_discs_sels then ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], []) else let val udiscs = map (rapp u) discs; val uselss = map (map (rapp u)) selss; val usel_ctrs = map2 (curry Term.list_comb) ctrs uselss; val usel_fs = map2 (curry Term.list_comb) fs uselss; val vdiscs = map (rapp v) discs; val vselss = map (map (rapp v)) selss; fun make_sel_thm xs' case_thm sel_def = zero_var_indexes (Variable.gen_all lthy (Drule.rename_bvars' (map (SOME o fst) xs') (Drule.forall_intr_vars (case_thm RS (sel_def RS trans))))); val sel_thmss = @{map 3} (map oo make_sel_thm) xss' case_thms sel_defss; fun has_undefined_rhs thm = (case snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of thm))) of Const (\<^const_name>\undefined\, _) => true | _ => false); val all_sel_thms = (if all_sels_distinct andalso null sel_default_eqs then flat sel_thmss else map_product (fn s => fn (xs', c) => make_sel_thm xs' c s) sel_defs (xss' ~~ case_thms)) |> filter_out has_undefined_rhs; fun mk_unique_disc_def () = let val m = the_single ms; val goal = mk_Trueprop_eq (mk_uu_eq (), the_single exist_xs_u_eq_ctrs); val vars = Variable.add_free_names lthy goal []; in Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_unique_disc_def_tac ctxt m uexhaust_thm) |> Thm.close_derivation \<^here> end; fun mk_alternate_disc_def k = let val goal = mk_Trueprop_eq (alternate_disc_lhs (K (nth udiscs)) (3 - k), nth exist_xs_u_eq_ctrs (k - 1)); val vars = Variable.add_free_names lthy goal []; in Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, ...} => mk_alternate_disc_def_tac ctxt k (nth disc_defs (2 - k)) (nth distinct_thms (2 - k)) uexhaust_thm) |> Thm.close_derivation \<^here> end; val has_alternate_disc_def = exists (fn def => Thm.eq_thm_prop (def, alternate_disc_no_def)) disc_defs; val nontriv_disc_defs = disc_defs |> filter_out (member Thm.eq_thm_prop [unique_disc_no_def, alternate_disc_no_def, refl]); val disc_defs' = map2 (fn k => fn def => if Thm.eq_thm_prop (def, unique_disc_no_def) then mk_unique_disc_def () else if Thm.eq_thm_prop (def, alternate_disc_no_def) then mk_alternate_disc_def k else def) ks disc_defs; val discD_thms = map (fn def => def RS iffD1) disc_defs'; val discI_thms = map2 (fn m => fn def => funpow m (fn thm => exI RS thm) (def RS iffD2)) ms disc_defs'; val not_discI_thms = map2 (fn m => fn def => funpow m (fn thm => allI RS thm) (unfold_thms lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]}))) ms disc_defs'; val (disc_thmss', disc_thmss) = let fun mk_thm discI _ [] = refl RS discI | mk_thm _ not_discI [distinct] = distinct RS not_discI; fun mk_thms discI not_discI distinctss = map (mk_thm discI not_discI) distinctss; in @{map 3} mk_thms discI_thms not_discI_thms distinct_thmsss' |> `transpose end; val nontriv_disc_thmss = map2 (fn b => if is_disc_binding_valid b then I else K []) disc_bindings disc_thmss; fun is_discI_triv b = (n = 1 andalso Binding.is_empty b) orelse Binding.eq_name (b, equal_binding); val nontriv_discI_thms = flat (map2 (fn b => if is_discI_triv b then K [] else single) disc_bindings discI_thms); val (distinct_disc_thms, (distinct_disc_thmsss', distinct_disc_thmsss)) = let fun mk_goal [] = [] | mk_goal [((_, udisc), (_, udisc'))] = [Logic.all u (Logic.mk_implies (HOLogic.mk_Trueprop udisc, HOLogic.mk_Trueprop (HOLogic.mk_not udisc')))]; fun prove tac goal = Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => tac ctxt) |> Thm.close_derivation \<^here>; val half_pairss = mk_half_pairss (`I (ms ~~ discD_thms ~~ udiscs)); val half_goalss = map mk_goal half_pairss; val half_thmss = @{map 3} (fn [] => K (K []) | [goal] => fn [(((m, discD), _), _)] => fn disc_thm => [prove (fn ctxt => mk_half_distinct_disc_tac ctxt m discD disc_thm) goal]) half_goalss half_pairss (flat disc_thmss'); val other_half_goalss = map (mk_goal o map swap) half_pairss; val other_half_thmss = map2 (map2 (fn thm => prove (fn ctxt => mk_other_half_distinct_disc_tac ctxt thm))) half_thmss other_half_goalss; in join_halves n half_thmss other_half_thmss ||> `transpose |>> has_alternate_disc_def ? K [] end; val exhaust_disc_thm = let fun mk_prem udisc = mk_imp_p [HOLogic.mk_Trueprop udisc]; val goal = fold_rev Logic.all [p, u] (mk_imp_p (map mk_prem udiscs)); in Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => mk_exhaust_disc_tac ctxt n exhaust_thm discI_thms) |> Thm.close_derivation \<^here> end; val (safe_collapse_thms, all_collapse_thms) = let fun mk_goal m udisc usel_ctr = let val prem = HOLogic.mk_Trueprop udisc; val concl = mk_Trueprop_eq ((usel_ctr, u) |> m = 0 ? swap); in (prem aconv concl, Logic.all u (Logic.mk_implies (prem, concl))) end; val (trivs, goals) = @{map 3} mk_goal ms udiscs usel_ctrs |> split_list; val thms = @{map 5} (fn m => fn discD => fn sel_thms => fn triv => fn goal => Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => mk_collapse_tac ctxt m discD sel_thms ORELSE HEADGOAL (assume_tac ctxt)) |> Thm.close_derivation \<^here> |> not triv ? perhaps (try (fn thm => refl RS thm))) ms discD_thms sel_thmss trivs goals; in (map_filter (fn (true, _) => NONE | (false, thm) => SOME thm) (trivs ~~ thms), thms) end; val swapped_all_collapse_thms = map2 (fn m => fn thm => if m = 0 then thm else thm RS sym) ms all_collapse_thms; val exhaust_sel_thm = let fun mk_prem usel_ctr = mk_imp_p [mk_Trueprop_eq (u, usel_ctr)]; val goal = fold_rev Logic.all [p, u] (mk_imp_p (map mk_prem usel_ctrs)); in Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => mk_exhaust_sel_tac ctxt n exhaust_disc_thm swapped_all_collapse_thms) |> Thm.close_derivation \<^here> end; val expand_thm = let fun mk_prems k udisc usels vdisc vsels = (if k = n then [] else [mk_Trueprop_eq (udisc, vdisc)]) @ (if null usels then [] else [Logic.list_implies (if n = 1 then [] else map HOLogic.mk_Trueprop [udisc, vdisc], HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) usels vsels)))]); val goal = Library.foldr Logic.list_implies (@{map 5} mk_prems ks udiscs uselss vdiscs vselss, uv_eq); val uncollapse_thms = map2 (fn thm => fn [] => thm | _ => thm RS sym) all_collapse_thms uselss; val vars = Variable.add_free_names lthy goal []; in Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => mk_expand_tac ctxt n ms (inst_thm u exhaust_disc_thm) (inst_thm v exhaust_disc_thm) uncollapse_thms distinct_disc_thmsss distinct_disc_thmsss') |> Thm.close_derivation \<^here> end; val (split_sel_thm, split_sel_asm_thm) = let val zss = map (K []) xss; val goal = mk_split_goal usel_ctrs zss usel_fs; val asm_goal = mk_split_asm_goal usel_ctrs zss usel_fs; val thm = prove_split sel_thmss goal; val asm_thm = prove_split_asm asm_goal thm; in (thm, asm_thm) end; val case_eq_if_thm = let val goal = mk_Trueprop_eq (ufcase, mk_IfN B udiscs usel_fs); val vars = Variable.add_free_names lthy goal []; in Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, ...} => mk_case_eq_if_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss) |> Thm.close_derivation \<^here> end; val disc_eq_case_thms = let fun const_of_bool b = if b then \<^const>\True\ else \<^const>\False\; fun mk_case_args n = map_index (fn (k, argTs) => fold_rev Term.absdummy argTs (const_of_bool (n = k))) ctr_Tss; val goals = map_index (fn (n, udisc) => mk_Trueprop_eq (udisc, list_comb (casexBool, mk_case_args n) $ u)) udiscs; val goal = Logic.mk_conjunction_balanced goals; val vars = Variable.add_free_names lthy goal []; in Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, ...} => mk_disc_eq_case_tac ctxt (Thm.cterm_of ctxt u) exhaust_thm (flat nontriv_disc_thmss) distinct_thms case_thms) |> Thm.close_derivation \<^here> |> Conjunction.elim_balanced (length goals) end; in (sel_defs, all_sel_thms, sel_thmss, nontriv_disc_defs, disc_thmss, nontriv_disc_thmss, discI_thms, nontriv_discI_thms, distinct_disc_thms, distinct_disc_thmsss, [exhaust_disc_thm], [exhaust_sel_thm], all_collapse_thms, safe_collapse_thms, [expand_thm], [split_sel_thm], [split_sel_asm_thm], [case_eq_if_thm], disc_eq_case_thms) end; val case_distrib_thm = let val args = @{map 2} (fn f => fn argTs => let val (args, _) = mk_Frees "x" argTs lthy in fold_rev Term.lambda args (h $ list_comb (f, args)) end) fs ctr_Tss; val goal = mk_Trueprop_eq (h $ ufcase, list_comb (casexC, args) $ u); val vars = Variable.add_free_names lthy goal []; in Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, ...} => mk_case_distrib_tac ctxt (Thm.cterm_of ctxt u) exhaust_thm case_thms) |> Thm.close_derivation \<^here> end; val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases)); val cases_type_attr = Attrib.internal (K (Induct.cases_type fcT_name)); val nontriv_disc_eq_thmss = map (map (fn th => th RS @{thm eq_False[THEN iffD2]} handle THM _ => th RS @{thm eq_True[THEN iffD2]})) nontriv_disc_thmss; val anonymous_notes = [(map (fn th => th RS notE) distinct_thms, safe_elim_attrs), (flat nontriv_disc_eq_thmss, nitpicksimp_attrs)] |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])])); val notes = [(caseN, case_thms, nitpicksimp_attrs @ simp_attrs), (case_congN, [case_cong_thm], []), (case_cong_weak_thmsN, [case_cong_weak_thm], cong_attrs), (case_distribN, [case_distrib_thm], []), (case_eq_ifN, case_eq_if_thms, []), (collapseN, safe_collapse_thms, if ms = [0] then [] else simp_attrs), (discN, flat nontriv_disc_thmss, simp_attrs), (disc_eq_caseN, disc_eq_case_thms, []), (discIN, nontriv_discI_thms, []), (distinctN, distinct_thms, simp_attrs @ inductsimp_attrs), (distinct_discN, distinct_disc_thms, dest_attrs), (exhaustN, [exhaust_thm], [exhaust_case_names_attr, cases_type_attr]), (exhaust_discN, exhaust_disc_thms, [exhaust_case_names_attr]), (exhaust_selN, exhaust_sel_thms, [exhaust_case_names_attr]), (expandN, expand_thms, []), (injectN, inject_thms, iff_attrs @ inductsimp_attrs), (nchotomyN, [nchotomy_thm], []), (selN, all_sel_thms, nitpicksimp_attrs @ simp_attrs), (splitN, [split_thm], []), (split_asmN, [split_asm_thm], []), (split_selN, split_sel_thms, []), (split_sel_asmN, split_sel_asm_thms, []), (split_selsN, split_sel_thms @ split_sel_asm_thms, []), (splitsN, [split_thm, split_asm_thm], [])] |> filter_out (null o #2) |> map (fn (thmN, thms, attrs) => ((qualify true (Binding.name thmN), attrs), [(thms, [])])); val (noted, lthy') = lthy |> Spec_Rules.add Binding.empty Spec_Rules.equational [casex] case_thms |> fold (uncurry (Spec_Rules.add Binding.empty Spec_Rules.equational)) (AList.group (eq_list (op aconv)) (map (`(single o lhs_head_of)) all_sel_thms)) |> fold (uncurry (Spec_Rules.add Binding.empty Spec_Rules.equational)) (filter_out (null o snd) (map single discs ~~ nontriv_disc_eq_thmss)) |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => Case_Translation.register (Morphism.term phi casex) (map (Morphism.term phi) ctrs)) |> plugins code_plugin ? (Code.declare_default_eqns (map (rpair true) (flat nontriv_disc_eq_thmss @ case_thms @ all_sel_thms)) #> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => Context.mapping (add_ctr_code fcT_name (map (Morphism.typ phi) As) (map (dest_Const o Morphism.term phi) ctrs) (Morphism.fact phi inject_thms) (Morphism.fact phi distinct_thms) (Morphism.fact phi case_thms)) I)) |> Local_Theory.notes (anonymous_notes @ notes) (* for "datatype_realizer.ML": *) |>> name_noted_thms fcT_name exhaustN; val ctr_sugar = {kind = kind, T = fcT, ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm, nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms, case_thms = case_thms, case_cong = case_cong_thm, case_cong_weak = case_cong_weak_thm, case_distribs = [case_distrib_thm], split = split_thm, split_asm = split_asm_thm, disc_defs = nontriv_disc_defs, disc_thmss = disc_thmss, discIs = discI_thms, disc_eq_cases = disc_eq_case_thms, sel_defs = sel_defs, sel_thmss = sel_thmss, distinct_discsss = distinct_disc_thmsss, exhaust_discs = exhaust_disc_thms, exhaust_sels = exhaust_sel_thms, collapses = all_collapse_thms, expands = expand_thms, split_sels = split_sel_thms, split_sel_asms = split_sel_asm_thms, case_eq_ifs = case_eq_if_thms} |> morph_ctr_sugar (substitute_noted_thm noted); in (ctr_sugar, lthy' |> register_ctr_sugar plugins ctr_sugar) end; in (goalss, after_qed, lthy) end; fun free_constructors kind tacss = (fn (goalss, after_qed, lthy) => map2 (map2 (Thm.close_derivation \<^here> oo Goal.prove_sorry lthy [] [])) goalss tacss |> (fn thms => after_qed thms lthy)) oo prepare_free_constructors kind (K I) (K I); fun free_constructors_cmd kind = (fn (goalss, after_qed, lthy) => Proof.theorem NONE (snd oo after_qed) (map (map (rpair [])) goalss) lthy) oo prepare_free_constructors kind Plugin_Name.make_filter Syntax.read_term; val parse_bound_term = Parse.binding --| \<^keyword>\:\ -- Parse.term; type ctr_options = Plugin_Name.filter * bool; type ctr_options_cmd = (Proof.context -> Plugin_Name.filter) * bool; val default_ctr_options : ctr_options = (Plugin_Name.default_filter, false); val default_ctr_options_cmd : ctr_options_cmd = (K Plugin_Name.default_filter, false); val parse_ctr_options = Scan.optional (\<^keyword>\(\ |-- Parse.list1 (Plugin_Name.parse_filter >> (apfst o K) || Parse.reserved "discs_sels" >> (apsnd o K o K true)) --| \<^keyword>\)\ >> (fn fs => fold I fs default_ctr_options_cmd)) default_ctr_options_cmd; fun parse_ctr_spec parse_ctr parse_arg = parse_opt_binding_colon -- parse_ctr -- Scan.repeat parse_arg; val parse_ctr_specs = Parse.enum1 "|" (parse_ctr_spec Parse.term Parse.binding); val parse_sel_default_eqs = Scan.optional (\<^keyword>\where\ |-- Parse.enum1 "|" Parse.prop) []; val _ = Outer_Syntax.local_theory_to_proof \<^command_keyword>\free_constructors\ "register an existing freely generated type's constructors" (parse_ctr_options -- Parse.binding --| \<^keyword>\for\ -- parse_ctr_specs -- parse_sel_default_eqs >> free_constructors_cmd Unknown); (** external views **) (* document antiquotations *) local fun antiquote_setup binding co = - Thy_Output.antiquotation_pretty_source_embedded binding + Document_Output.antiquotation_pretty_source_embedded binding ((Scan.ahead (Scan.lift Parse.not_eof) >> Token.pos_of) -- Args.type_name {proper = true, strict = true}) (fn ctxt => fn (pos, type_name) => let fun err () = error ("Bad " ^ Binding.name_of binding ^ ": " ^ quote type_name ^ Position.here pos); in (case ctr_sugar_of ctxt type_name of NONE => err () | SOME {kind, T = T0, ctrs = ctrs0, ...} => let val _ = if co = (kind = Codatatype) then () else err (); val T = Logic.unvarifyT_global T0; val ctrs = map Logic.unvarify_global ctrs0; val pretty_typ_bracket = Syntax.pretty_typ (Config.put pretty_priority 1001 ctxt); fun pretty_ctr ctr = Pretty.block (Pretty.breaks (Syntax.pretty_term ctxt ctr :: map pretty_typ_bracket (binder_types (fastype_of ctr)))); in Pretty.block (Pretty.keyword1 (Binding.name_of binding) :: Pretty.brk 1 :: Syntax.pretty_typ ctxt T :: Pretty.str " =" :: Pretty.brk 1 :: flat (separate [Pretty.brk 1, Pretty.str "| "] (map (single o pretty_ctr) ctrs))) end) end); in val _ = Theory.setup (antiquote_setup \<^binding>\datatype\ false #> antiquote_setup \<^binding>\codatatype\ true); end; (* theory export *) val _ = Export_Theory.setup_presentation (fn context => fn thy => let val parents = map (Data.get o Context.Theory) (Theory.parents_of thy); val datatypes = (Data.get (Context.Theory thy), []) |-> Symtab.fold (fn (name, (pos, {kind, T, ctrs, ...})) => if kind = Record orelse exists (fn tab => Symtab.defined tab name) parents then I else let val pos_properties = Thy_Info.adjust_pos_properties context pos; val typ = Logic.unvarifyT_global T; val constrs = map Logic.unvarify_global ctrs; val typargs = rev (fold Term.add_tfrees (Logic.mk_type typ :: constrs) []); val constructors = map (fn t => (t, Term.type_of t)) constrs; in cons (pos_properties, (name, (kind = Codatatype, (typargs, (typ, constructors))))) end); in if null datatypes then () else Export_Theory.export_body thy "datatypes" let open XML.Encode Term_XML.Encode in list (pair properties (pair string (pair bool (pair (list (pair string sort)) (pair typ (list (pair (term (Sign.consts_of thy)) typ))))))) datatypes end end); end; diff --git a/src/HOL/Tools/value_command.ML b/src/HOL/Tools/value_command.ML --- a/src/HOL/Tools/value_command.ML +++ b/src/HOL/Tools/value_command.ML @@ -1,84 +1,84 @@ (* Title: HOL/Tools/value_command.ML Author: Florian Haftmann, TU Muenchen Generic value command for arbitrary evaluators, with default using nbe or SML. *) signature VALUE_COMMAND = sig val value: Proof.context -> term -> term val value_select: string -> Proof.context -> term -> term val value_cmd: xstring -> string list -> string -> Toplevel.state -> unit val add_evaluator: binding * (Proof.context -> term -> term) -> theory -> string * theory end; structure Value_Command : VALUE_COMMAND = struct structure Evaluators = Theory_Data ( type T = (Proof.context -> term -> term) Name_Space.table; val empty = Name_Space.empty_table "evaluator"; val extend = I; val merge = Name_Space.merge_tables; ) fun add_evaluator (b, evaluator) thy = let val (name, tab') = Name_Space.define (Context.Theory thy) true (b, evaluator) (Evaluators.get thy); val thy' = Evaluators.put tab' thy; in (name, thy') end; fun intern_evaluator ctxt raw_name = if raw_name = "" then "" else Name_Space.intern (Name_Space.space_of_table (Evaluators.get (Proof_Context.theory_of ctxt))) raw_name; fun default_value ctxt t = if null (Term.add_frees t []) then Code_Evaluation.dynamic_value_strict ctxt t else Nbe.dynamic_value ctxt t; fun value_select name ctxt = if name = "" then default_value ctxt else Name_Space.get (Evaluators.get (Proof_Context.theory_of ctxt)) name ctxt; val value = value_select ""; fun value_cmd raw_name modes raw_t state = let val ctxt = Toplevel.context_of state; val name = intern_evaluator ctxt raw_name; val t = Syntax.read_term ctxt raw_t; val t' = value_select name ctxt t; val ty' = Term.type_of t'; val ctxt' = Proof_Context.augment t' ctxt; val p = Print_Mode.with_modes modes (fn () => Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk, Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) (); in Pretty.writeln p end; val opt_modes = Scan.optional (\<^keyword>\(\ |-- Parse.!!! (Scan.repeat1 Parse.name --| \<^keyword>\)\)) []; val opt_evaluator = Scan.optional (\<^keyword>\[\ |-- Parse.name --| \<^keyword>\]\) ""; val _ = Outer_Syntax.command \<^command_keyword>\value\ "evaluate and print term" (opt_evaluator -- opt_modes -- Parse.term >> (fn ((name, modes), t) => Toplevel.keep (value_cmd name modes t))); val _ = Theory.setup - (Thy_Output.antiquotation_pretty_source_embedded \<^binding>\value\ + (Document_Output.antiquotation_pretty_source_embedded \<^binding>\value\ (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term) (fn ctxt => fn ((name, style), t) => - Thy_Output.pretty_term ctxt (style (value_select name ctxt t))) + Document_Output.pretty_term ctxt (style (value_select name ctxt t))) #> add_evaluator (\<^binding>\simp\, Code_Simp.dynamic_value) #> snd #> add_evaluator (\<^binding>\nbe\, Nbe.dynamic_value) #> snd #> add_evaluator (\<^binding>\code\, Code_Evaluation.dynamic_value_strict) #> snd); end; diff --git a/src/Pure/ML/ml_file.ML b/src/Pure/ML/ml_file.ML --- a/src/Pure/ML/ml_file.ML +++ b/src/Pure/ML/ml_file.ML @@ -1,39 +1,39 @@ (* Title: Pure/ML/ml_file.ML Author: Makarius Commands to load ML files. *) signature ML_FILE = sig val command: string -> bool option -> (theory -> Token.file) -> Toplevel.transition -> Toplevel.transition val ML: bool option -> (theory -> Token.file) -> Toplevel.transition -> Toplevel.transition val SML: bool option -> (theory -> Token.file) -> Toplevel.transition -> Toplevel.transition end; structure ML_File: ML_FILE = struct fun command environment debug get_file = Toplevel.generic_theory (fn gthy => let val file = get_file (Context.theory_of gthy); val provide = Resources.provide_file file; val source = Token.file_source file; - val _ = Thy_Output.check_comments (Context.proof_of gthy) (Input.source_explode source); + val _ = Document_Output.check_comments (Context.proof_of gthy) (Input.source_explode source); val flags: ML_Compiler.flags = {environment = environment, redirect = true, verbose = true, debug = debug, writeln = writeln, warning = warning}; in gthy |> ML_Context.exec (fn () => ML_Context.eval_source flags source) |> Local_Theory.propagate_ml_env |> Context.mapping provide (Local_Theory.background_theory provide) end); val ML = command ""; val SML = command ML_Env.SML; end; diff --git a/src/Pure/PIDE/command.ML b/src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML +++ b/src/Pure/PIDE/command.ML @@ -1,507 +1,507 @@ (* Title: Pure/PIDE/command.ML Author: Makarius Prover command execution: read -- eval -- print. *) signature COMMAND = sig type blob = {file_node: string, src_path: Path.T, content: (SHA1.digest * string list) option} val read_file: Path.T -> Position.T -> bool -> Path.T -> Token.file val read_thy: Toplevel.state -> theory val read: Keyword.keywords -> theory -> Path.T-> (unit -> theory) -> blob Exn.result list * int -> Token.T list -> Toplevel.transition val read_span: Keyword.keywords -> Toplevel.state -> Path.T -> (unit -> theory) -> Command_Span.span -> Toplevel.transition type eval val eval_command_id: eval -> Document_ID.command val eval_exec_id: eval -> Document_ID.exec val eval_eq: eval * eval -> bool val eval_running: eval -> bool val eval_finished: eval -> bool val eval_result_command: eval -> Toplevel.transition val eval_result_state: eval -> Toplevel.state val eval: Keyword.keywords -> Path.T -> (unit -> theory) -> blob Exn.result list * int -> Document_ID.command -> Token.T list -> eval -> eval type print type print_fn = Toplevel.transition -> Toplevel.state -> unit val print0: {pri: int, print_fn: print_fn} -> eval -> print val print: bool -> (string * string list) list -> Keyword.keywords -> string -> eval -> print list -> print list option val parallel_print: print -> bool type print_function = {keywords: Keyword.keywords, command_name: string, args: string list, exec_id: Document_ID.exec} -> {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option val print_function: string -> print_function -> unit val no_print_function: string -> unit type exec = eval * print list val init_exec: theory option -> exec val no_exec: exec val exec_ids: exec option -> Document_ID.exec list val exec: Document_ID.execution -> exec -> unit val exec_parallel_prints: Document_ID.execution -> Future.task list -> exec -> exec option end; structure Command: COMMAND = struct (** main phases of execution **) fun task_context group f = f |> Future.interruptible_task |> Future.task_context "Command.run_process" group; (* read *) type blob = {file_node: string, src_path: Path.T, content: (SHA1.digest * string list) option}; fun read_file_node file_node master_dir pos delimited src_path = let val _ = if Context_Position.pide_reports () then Position.report pos (Markup.language_path delimited) else (); fun read_file () = let val path = File.check_file (File.full_path master_dir src_path); val text = File.read path; val file_pos = Path.position path; in (text, file_pos) end; fun read_url () = let val text = Isabelle_System.download file_node; val file_pos = Position.file file_node; in (text, file_pos) end; val (text, file_pos) = (case try Url.explode file_node of NONE => read_file () | SOME (Url.File _) => read_file () | _ => read_url ()); val lines = split_lines text; val digest = SHA1.digest text; in {src_path = src_path, lines = lines, digest = digest, pos = Position.copy_id pos file_pos} end handle ERROR msg => error (msg ^ Position.here pos); val read_file = read_file_node ""; local fun blob_file src_path lines digest file_node = let val file_pos = Position.file file_node |> (case Position.get_id (Position.thread_data ()) of NONE => I | SOME exec_id => Position.put_id exec_id); in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end fun resolve_files master_dir (blobs, blobs_index) toks = (case Outer_Syntax.parse_spans toks of [Command_Span.Span (Command_Span.Command_Span _, _)] => (case try (nth toks) blobs_index of SOME tok => let val source = Token.input_of tok; val pos = Input.pos_of source; val delimited = Input.is_delimited source; fun make_file (Exn.Res {file_node, src_path, content = NONE}) = Exn.interruptible_capture (fn () => read_file_node file_node master_dir pos delimited src_path) () | make_file (Exn.Res {file_node, src_path, content = SOME (digest, lines)}) = (Position.report pos (Markup.language_path delimited); Exn.Res (blob_file src_path lines digest file_node)) | make_file (Exn.Exn e) = Exn.Exn e; val files = map make_file blobs; in toks |> map_index (fn (i, tok) => if i = blobs_index then Token.put_files files tok else tok) end | NONE => toks) | _ => toks); fun reports_of_token keywords tok = let val malformed_symbols = Input.source_explode (Token.input_of tok) |> map_filter (fn (sym, pos) => if Symbol.is_malformed sym then SOME ((pos, Markup.bad ()), "Malformed symbolic character") else NONE); val is_malformed = Token.is_error tok orelse not (null malformed_symbols); val reports = Token.reports keywords tok @ Token.completion_report tok @ malformed_symbols; in (is_malformed, reports) end; in fun read_thy st = Toplevel.theory_of st handle Toplevel.UNDEF => Pure_Syn.bootstrap_thy; fun read keywords thy master_dir init blobs_info span = let val command_reports = Outer_Syntax.command_reports thy; val token_reports = map (reports_of_token keywords) span; val _ = Position.reports_text (maps #2 token_reports @ maps command_reports span); val verbatim = span |> map_filter (fn tok => if Token.kind_of tok = Token.Verbatim then SOME (Token.pos_of tok) else NONE); val _ = if null verbatim then () else legacy_feature ("Old-style {* verbatim *} token -- use \cartouche\ instead" ^ Position.here_list verbatim); in if exists #1 token_reports then Toplevel.malformed (#1 (Token.core_range_of span)) "Malformed command syntax" else Outer_Syntax.parse_span thy init (resolve_files master_dir blobs_info span) end; end; fun read_span keywords st master_dir init = Command_Span.content #> read keywords (read_thy st) master_dir init ([], ~1); (* eval *) type eval_state = {failed: bool, command: Toplevel.transition, state: Toplevel.state}; fun init_eval_state opt_thy = {failed = false, command = Toplevel.empty, state = (case opt_thy of NONE => Toplevel.init_toplevel () | SOME thy => Toplevel.theory_toplevel thy)}; datatype eval = Eval of {command_id: Document_ID.command, exec_id: Document_ID.exec, eval_process: eval_state lazy}; fun eval_command_id (Eval {command_id, ...}) = command_id; fun eval_exec_id (Eval {exec_id, ...}) = exec_id; val eval_eq = op = o apply2 eval_exec_id; val eval_running = Execution.is_running_exec o eval_exec_id; fun eval_finished (Eval {eval_process, ...}) = Lazy.is_finished eval_process; fun eval_result (Eval {eval_process, ...}) = Exn.release (Lazy.finished_result eval_process); val eval_result_command = #command o eval_result; val eval_result_state = #state o eval_result; local fun reset_state keywords tr st0 = Toplevel.setmp_thread_position tr (fn () => let val name = Toplevel.name_of tr; val res = if Keyword.is_theory_body keywords name then Toplevel.reset_theory st0 else if Keyword.is_proof keywords name then Toplevel.reset_proof st0 else if Keyword.is_theory_end keywords name then (case Toplevel.reset_notepad st0 of NONE => Toplevel.reset_theory st0 | some => some) else NONE; in (case res of NONE => st0 | SOME st => (Output.error_message (Toplevel.type_error tr ^ " -- using reset state"); st)) end) (); fun run keywords int tr st = if Future.proofs_enabled 1 andalso Keyword.is_diag keywords (Toplevel.name_of tr) then let val (tr1, tr2) = Toplevel.fork_presentation tr; val _ = Execution.fork {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1} (fn () => Toplevel.command_exception int tr1 st); in Toplevel.command_errors int tr2 st end else Toplevel.command_errors int tr st; fun check_token_comments ctxt tok = - (Thy_Output.check_comments ctxt (Input.source_explode (Token.input_of tok)); []) + (Document_Output.check_comments ctxt (Input.source_explode (Token.input_of tok)); []) handle exn => if Exn.is_interrupt exn then Exn.reraise exn else Runtime.exn_messages exn; fun check_span_comments ctxt span tr = Toplevel.setmp_thread_position tr (fn () => maps (check_token_comments ctxt) span) (); fun report_indent tr st = (case try Toplevel.proof_of st of SOME prf => let val keywords = Thy_Header.get_keywords (Proof.theory_of prf) in if Keyword.command_kind keywords (Toplevel.name_of tr) = SOME Keyword.prf_script then (case try (Thm.nprems_of o #goal o Proof.goal) prf of NONE => () | SOME 0 => () | SOME n => let val report = Markup.markup_only (Markup.command_indent (n - 1)); in Toplevel.setmp_thread_position tr (fn () => Output.report [report]) () end) else () end | NONE => ()); fun status tr m = Toplevel.setmp_thread_position tr (fn () => Output.status [Markup.markup_only m]) (); fun eval_state keywords span tr ({state, ...}: eval_state) = let val _ = Thread_Attributes.expose_interrupt (); val st = reset_state keywords tr state; val _ = report_indent tr st; val _ = status tr Markup.running; val (errs1, result) = run keywords true tr st; val errs2 = (case result of NONE => [] | SOME st' => check_span_comments (Toplevel.presentation_context st') span tr); val errs = errs1 @ errs2; val _ = List.app (Future.error_message (Toplevel.pos_of tr)) errs; in (case result of NONE => let val _ = status tr Markup.failed; val _ = status tr Markup.finished; val _ = if null errs then (status tr Markup.canceled; Exn.interrupt ()) else (); in {failed = true, command = tr, state = st} end | SOME st' => let val _ = if Keyword.is_theory_end keywords (Toplevel.name_of tr) andalso can (Toplevel.end_theory Position.none) st' then status tr Markup.finalized else (); val _ = status tr Markup.finished; in {failed = false, command = tr, state = st'} end) end; in fun eval keywords master_dir init blobs_info command_id span eval0 = let val exec_id = Document_ID.make (); fun process () = let val eval_state0 = eval_result eval0; val thy = read_thy (#state eval_state0); val tr = Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id)) (fn () => read keywords thy master_dir init blobs_info span |> Toplevel.exec_id exec_id) (); in eval_state keywords span tr eval_state0 end; in Eval {command_id = command_id, exec_id = exec_id, eval_process = Lazy.lazy_name "Command.eval" process} end; end; (* print *) datatype print = Print of {name: string, args: string list, delay: Time.time option, pri: int, persistent: bool, exec_id: Document_ID.exec, print_process: unit lazy}; fun print_exec_id (Print {exec_id, ...}) = exec_id; val print_eq = op = o apply2 print_exec_id; type print_fn = Toplevel.transition -> Toplevel.state -> unit; type print_function = {keywords: Keyword.keywords, command_name: string, args: string list, exec_id: Document_ID.exec} -> {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option; local val print_functions = Synchronized.var "Command.print_functions" ([]: (string * print_function) list); fun print_error tr opt_context e = (Toplevel.setmp_thread_position tr o Runtime.controlled_execution opt_context) e () handle exn => if Exn.is_interrupt exn then Exn.reraise exn else List.app (Future.error_message (Toplevel.pos_of tr)) (Runtime.exn_messages exn); fun print_finished (Print {print_process, ...}) = Lazy.is_finished print_process; fun print_persistent (Print {persistent, ...}) = persistent; val overlay_ord = prod_ord string_ord (list_ord string_ord); fun make_print (name, args) {delay, pri, persistent, strict, print_fn} eval = let val exec_id = Document_ID.make (); fun process () = let val {failed, command, state = st', ...} = eval_result eval; val tr = Toplevel.exec_id exec_id command; val opt_context = try Toplevel.generic_theory_of st'; in if failed andalso strict then () else print_error tr opt_context (fn () => print_fn tr st') end; in Print { name = name, args = args, delay = delay, pri = pri, persistent = persistent, exec_id = exec_id, print_process = Lazy.lazy_name "Command.print" process} end; fun bad_print name_args exn = make_print name_args {delay = NONE, pri = 0, persistent = false, strict = false, print_fn = fn _ => fn _ => Exn.reraise exn}; in fun print0 {pri, print_fn} = make_print ("", [serial_string ()]) {delay = NONE, pri = pri, persistent = true, strict = true, print_fn = print_fn}; fun print command_visible command_overlays keywords command_name eval old_prints = let val print_functions = Synchronized.value print_functions; fun new_print (name, args) get_pr = let val params = {keywords = keywords, command_name = command_name, args = args, exec_id = eval_exec_id eval}; in (case Exn.capture (Runtime.controlled_execution NONE get_pr) params of Exn.Res NONE => NONE | Exn.Res (SOME pr) => SOME (make_print (name, args) pr eval) | Exn.Exn exn => SOME (bad_print (name, args) exn eval)) end; fun get_print (name, args) = (case find_first (fn Print print => (#name print, #args print) = (name, args)) old_prints of NONE => (case AList.lookup (op =) print_functions name of NONE => SOME (bad_print (name, args) (ERROR ("Missing print function " ^ quote name)) eval) | SOME get_pr => new_print (name, args) get_pr) | some => some); val retained_prints = filter (fn print => print_finished print andalso print_persistent print) old_prints; val visible_prints = if command_visible then fold (fn (name, _) => cons (name, [])) print_functions command_overlays |> sort_distinct overlay_ord |> map_filter get_print else []; val new_prints = visible_prints @ retained_prints; in if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints end; fun parallel_print (Print {pri, ...}) = pri <= 0 orelse (Future.enabled () andalso Options.default_bool "parallel_print"); fun print_function name f = Synchronized.change print_functions (fn funs => (if name = "" then error "Unnamed print function" else (); if not (AList.defined (op =) funs name) then () else warning ("Redefining command print function: " ^ quote name); AList.update (op =) (name, f) funs)); fun no_print_function name = Synchronized.change print_functions (filter_out (equal name o #1)); end; val _ = print_function "Execution.print" (fn {args, exec_id, ...} => if null args then SOME {delay = NONE, pri = Task_Queue.urgent_pri + 2, persistent = false, strict = false, print_fn = fn _ => fn _ => Execution.fork_prints exec_id} else NONE); val _ = print_function "print_state" (fn {keywords, command_name, ...} => if Options.default_bool "editor_output_state" andalso Keyword.is_printed keywords command_name then SOME {delay = NONE, pri = Task_Queue.urgent_pri + 1, persistent = false, strict = false, print_fn = fn _ => fn st => if Toplevel.is_proof st then Output.state (Toplevel.string_of_state st) else ()} else NONE); (* combined execution *) type exec = eval * print list; fun init_exec opt_thy : exec = (Eval {command_id = Document_ID.none, exec_id = Document_ID.none, eval_process = Lazy.value (init_eval_state opt_thy)}, []); val no_exec = init_exec NONE; fun exec_ids NONE = [] | exec_ids (SOME (eval, prints)) = eval_exec_id eval :: map print_exec_id prints; local fun run_process execution_id exec_id process = let val group = Future.worker_subgroup () in if Execution.running execution_id exec_id [group] then ignore (task_context group (fn () => Lazy.force_result {strict = true} process) ()) else () end; fun ignore_process process = Lazy.is_running process orelse Lazy.is_finished process; fun run_eval execution_id (Eval {exec_id, eval_process, ...}) = if Lazy.is_finished eval_process then () else run_process execution_id exec_id eval_process; fun fork_print execution_id deps (Print {name, delay, pri, exec_id, print_process, ...}) = let val group = Future.worker_subgroup (); fun fork () = ignore ((singleton o Future.forks) {name = name, group = SOME group, deps = deps, pri = pri, interrupts = true} (fn () => if ignore_process print_process then () else run_process execution_id exec_id print_process)); in (case delay of NONE => fork () | SOME d => ignore (Event_Timer.request {physical = true} (Time.now () + d) fork)) end; fun run_print execution_id (print as Print {exec_id, print_process, ...}) = if ignore_process print_process then () else if parallel_print print then fork_print execution_id [] print else run_process execution_id exec_id print_process; in fun exec execution_id (eval, prints) = (run_eval execution_id eval; List.app (run_print execution_id) prints); fun exec_parallel_prints execution_id deps (exec as (Eval {eval_process, ...}, prints)) = if Lazy.is_finished eval_process then (List.app (fork_print execution_id deps) prints; NONE) else SOME exec; end; end; diff --git a/src/Pure/PIDE/resources.ML b/src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML +++ b/src/Pure/PIDE/resources.ML @@ -1,443 +1,443 @@ (* Title: Pure/PIDE/resources.ML Author: Makarius Resources for theories and auxiliary files. *) signature RESOURCES = sig val default_qualifier: string val init_session: {session_positions: (string * Properties.T) list, session_directories: (string * string) list, session_chapters: (string * string) list, bibtex_entries: (string * string list) list, command_timings: Properties.T list, scala_functions: (string * (bool * Position.T)) list, global_theories: (string * string) list, loaded_theories: string list} -> unit val init_session_yxml: string -> unit val init_session_file: Path.T -> unit val finish_session_base: unit -> unit val global_theory: string -> string option val loaded_theory: string -> bool val check_session: Proof.context -> string * Position.T -> string val session_chapter: string -> string val last_timing: Toplevel.transition -> Time.time val scala_functions: unit -> string list val check_scala_function: Proof.context -> string * Position.T -> string * bool val master_directory: theory -> Path.T val imports_of: theory -> (string * Position.T) list val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory val thy_path: Path.T -> Path.T val theory_qualifier: string -> string val theory_bibtex_entries: string -> string list val find_theory_file: string -> Path.T option val import_name: string -> Path.T -> string -> {node_name: Path.T, master_dir: Path.T, theory_name: string} val check_thy: Path.T -> string -> {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T, imports: (string * Position.T) list, keywords: Thy_Header.keywords} val parse_files: (Path.T -> Path.T list) -> (theory -> Token.file list) parser val parse_file: (theory -> Token.file) parser val provide: Path.T * SHA1.digest -> theory -> theory val provide_file: Token.file -> theory -> theory val provide_parse_files: (Path.T -> Path.T list) -> (theory -> Token.file list * theory) parser val provide_parse_file: (theory -> Token.file * theory) parser val loaded_files_current: theory -> bool val check_path: Proof.context -> Path.T option -> Input.source -> Path.T val check_file: Proof.context -> Path.T option -> Input.source -> Path.T val check_dir: Proof.context -> Path.T option -> Input.source -> Path.T val check_session_dir: Proof.context -> Path.T option -> Input.source -> Path.T end; structure Resources: RESOURCES = struct (* command timings *) type timings = ((string * Time.time) Inttab.table) Symtab.table; (*file -> offset -> name, time*) val empty_timings: timings = Symtab.empty; fun update_timings props = (case Markup.parse_command_timing_properties props of SOME ({file, offset, name}, time) => Symtab.map_default (file, Inttab.empty) (Inttab.map_default (offset, (name, time)) (fn (_, t) => (name, t + time))) | NONE => I); fun make_timings command_timings = fold update_timings command_timings empty_timings; fun approximative_id name pos = (case (Position.file_of pos, Position.offset_of pos) of (SOME file, SOME offset) => if name = "" then NONE else SOME {file = file, offset = offset, name = name} | _ => NONE); fun get_timings timings tr = (case approximative_id (Toplevel.name_of tr) (Toplevel.pos_of tr) of SOME {file, offset, name} => (case Symtab.lookup timings file of SOME offsets => (case Inttab.lookup offsets offset of SOME (name', time) => if name = name' then SOME time else NONE | NONE => NONE) | NONE => NONE) | NONE => NONE) |> the_default Time.zeroTime; (* session base *) val default_qualifier = "Draft"; type entry = {pos: Position.T, serial: serial}; fun make_entry props : entry = {pos = Position.of_properties props, serial = serial ()}; val empty_session_base = ({session_positions = []: (string * entry) list, session_directories = Symtab.empty: Path.T list Symtab.table, session_chapters = Symtab.empty: string Symtab.table, bibtex_entries = Symtab.empty: string list Symtab.table, timings = empty_timings, scala_functions = Symtab.empty: (bool * Position.T) Symtab.table}, {global_theories = Symtab.empty: string Symtab.table, loaded_theories = Symtab.empty: unit Symtab.table}); val global_session_base = Synchronized.var "Sessions.base" empty_session_base; fun init_session {session_positions, session_directories, session_chapters, bibtex_entries, command_timings, scala_functions, global_theories, loaded_theories} = Synchronized.change global_session_base (fn _ => ({session_positions = sort_by #1 (map (apsnd make_entry) session_positions), session_directories = fold_rev (fn (dir, name) => Symtab.cons_list (name, Path.explode dir)) session_directories Symtab.empty, session_chapters = Symtab.make session_chapters, bibtex_entries = Symtab.make bibtex_entries, timings = make_timings command_timings, scala_functions = Symtab.make scala_functions}, {global_theories = Symtab.make global_theories, loaded_theories = Symtab.make_set loaded_theories})); fun init_session_yxml yxml = let val (session_positions, (session_directories, (session_chapters, (bibtex_entries, (command_timings, (scala_functions, (global_theories, loaded_theories))))))) = YXML.parse_body yxml |> let open XML.Decode in (pair (list (pair string properties)) (pair (list (pair string string)) (pair (list (pair string string)) (pair (list (pair string (list string))) (pair (list properties) (pair (list (pair string (pair bool properties))) (pair (list (pair string string)) (list string)))))))) end; in init_session {session_positions = session_positions, session_directories = session_directories, session_chapters = session_chapters, bibtex_entries = bibtex_entries, command_timings = command_timings, scala_functions = (map o apsnd o apsnd) Position.of_properties scala_functions, global_theories = global_theories, loaded_theories = loaded_theories} end; fun init_session_file path = init_session_yxml (File.read path) before File.rm path; fun finish_session_base () = Synchronized.change global_session_base (apfst (K (#1 empty_session_base))); fun get_session_base f = f (Synchronized.value global_session_base); fun get_session_base1 f = get_session_base (f o #1); fun get_session_base2 f = get_session_base (f o #2); fun global_theory a = Symtab.lookup (get_session_base2 #global_theories) a; fun loaded_theory a = Symtab.defined (get_session_base2 #loaded_theories) a; fun check_session ctxt arg = Completion.check_item "session" (fn (name, {pos, serial}) => Markup.entity Markup.sessionN name |> Markup.properties (Position.entity_properties_of false serial pos)) (get_session_base1 #session_positions) ctxt arg; fun session_chapter name = the_default "Unsorted" (Symtab.lookup (get_session_base1 #session_chapters) name); fun last_timing tr = get_timings (get_session_base1 #timings) tr; (* Scala functions *) (*raw bootstrap environment*) fun scala_functions () = space_explode "," (getenv "ISABELLE_SCALA_FUNCTIONS"); (*regular resources*) fun scala_function a = (a, the_default (false, Position.none) (Symtab.lookup (get_session_base1 #scala_functions) a)); fun check_scala_function ctxt arg = let val funs = scala_functions () |> sort_strings |> map scala_function; val name = Completion.check_entity Markup.scala_functionN (map (apsnd #2) funs) ctxt arg; val multi = (case AList.lookup (op =) funs name of SOME (multi, _) => multi | NONE => false); in (name, multi) end; val _ = Theory.setup - (Thy_Output.antiquotation_verbatim_embedded \<^binding>\scala_function\ + (Document_Output.antiquotation_verbatim_embedded \<^binding>\scala_function\ (Scan.lift Parse.embedded_position) (#1 oo check_scala_function) #> ML_Antiquotation.inline_embedded \<^binding>\scala_function\ (Args.context -- Scan.lift Parse.embedded_position >> (uncurry check_scala_function #> #1 #> ML_Syntax.print_string)) #> ML_Antiquotation.value_embedded \<^binding>\scala\ (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) => let val (name, multi) = check_scala_function ctxt arg; val func = if multi then "Scala.function" else "Scala.function1"; in ML_Syntax.atomic (func ^ " " ^ ML_Syntax.print_string name) end))); (* manage source files *) type files = {master_dir: Path.T, (*master directory of theory source*) imports: (string * Position.T) list, (*source specification of imports*) provided: (Path.T * SHA1.digest) list}; (*source path, digest*) fun make_files (master_dir, imports, provided): files = {master_dir = master_dir, imports = imports, provided = provided}; structure Files = Theory_Data ( type T = files; val empty = make_files (Path.current, [], []); val extend = I; fun merge ({master_dir, imports, provided = provided1}, {provided = provided2, ...}) = let val provided' = Library.merge (op =) (provided1, provided2) in make_files (master_dir, imports, provided') end ); fun map_files f = Files.map (fn {master_dir, imports, provided} => make_files (f (master_dir, imports, provided))); val master_directory = #master_dir o Files.get; val imports_of = #imports o Files.get; fun begin_theory master_dir {name, imports, keywords} parents = Theory.begin_theory name parents |> map_files (fn _ => (Path.explode (Path.implode_symbolic master_dir), imports, [])) |> Thy_Header.add_keywords keywords; (* theory files *) val thy_path = Path.ext "thy"; fun theory_qualifier theory = (case global_theory theory of SOME qualifier => qualifier | NONE => Long_Name.qualifier theory); fun theory_name qualifier theory = if Long_Name.is_qualified theory orelse is_some (global_theory theory) then theory else Long_Name.qualify qualifier theory; fun theory_bibtex_entries theory = Symtab.lookup_list (get_session_base1 #bibtex_entries) (theory_qualifier theory); fun find_theory_file thy_name = let val thy_file = thy_path (Path.basic (Long_Name.base_name thy_name)); val session = theory_qualifier thy_name; val dirs = Symtab.lookup_list (get_session_base1 #session_directories) session; in dirs |> get_first (fn dir => let val path = dir + thy_file in if File.is_file path then SOME path else NONE end) end; fun make_theory_node node_name theory = {node_name = node_name, master_dir = Path.dir node_name, theory_name = theory}; fun loaded_theory_node theory = {node_name = Path.basic theory, master_dir = Path.current, theory_name = theory}; fun import_name qualifier dir s = let val theory = theory_name qualifier (Thy_Header.import_name s); fun theory_node () = make_theory_node (File.full_path dir (thy_path (Path.expand (Path.explode s)))) theory; in if not (Thy_Header.is_base_name s) then theory_node () else if loaded_theory theory then loaded_theory_node theory else (case find_theory_file theory of SOME node_name => make_theory_node node_name theory | NONE => if Long_Name.is_qualified s then loaded_theory_node theory else theory_node ()) end; fun check_file dir file = File.check_file (File.full_path dir file); fun check_thy dir thy_name = let val thy_base_name = Long_Name.base_name thy_name; val master_file = (case find_theory_file thy_name of SOME path => check_file Path.current path | NONE => check_file dir (thy_path (Path.basic thy_base_name))); val text = File.read master_file; val {name = (name, pos), imports, keywords} = Thy_Header.read (Path.position master_file) text; val _ = thy_base_name <> name andalso error ("Bad theory name " ^ quote name ^ " for file " ^ Path.print (Path.base master_file) ^ Position.here pos); in {master = (master_file, SHA1.digest text), text = text, theory_pos = pos, imports = imports, keywords = keywords} end; (* load files *) fun parse_files make_paths = Scan.ahead Parse.not_eof -- Parse.path_input >> (fn (tok, source) => fn thy => (case Token.get_files tok of [] => let val master_dir = master_directory thy; val name = Input.string_of source; val pos = Input.pos_of source; val delimited = Input.is_delimited source; val src_paths = make_paths (Path.explode name); in map (Command.read_file master_dir pos delimited) src_paths end | files => map Exn.release files)); val parse_file = parse_files single >> (fn f => f #> the_single); fun provide (src_path, id) = map_files (fn (master_dir, imports, provided) => if AList.defined (op =) provided src_path then error ("Duplicate use of source file: " ^ Path.print src_path) else (master_dir, imports, (src_path, id) :: provided)); fun provide_file (file: Token.file) = provide (#src_path file, #digest file); fun provide_parse_files make_paths = parse_files make_paths >> (fn files => fn thy => let val fs = files thy; val thy' = fold (fn {src_path, digest, ...} => provide (src_path, digest)) fs thy; in (fs, thy') end); val provide_parse_file = provide_parse_files single >> (fn f => f #>> the_single); fun load_file thy src_path = let val full_path = check_file (master_directory thy) src_path; val text = File.read full_path; val id = SHA1.digest text; in ((full_path, id), text) end; fun loaded_files_current thy = #provided (Files.get thy) |> forall (fn (src_path, id) => (case try (load_file thy) src_path of NONE => false | SOME ((_, id'), _) => id = id')); (* formal check *) fun formal_check check_file ctxt opt_dir source = let val name = Input.string_of source; val pos = Input.pos_of source; val delimited = Input.is_delimited source; val _ = Context_Position.report ctxt pos (Markup.language_path delimited); fun err msg = error (msg ^ Position.here pos); val dir = (case opt_dir of SOME dir => dir | NONE => master_directory (Proof_Context.theory_of ctxt)); val path = dir + Path.explode name handle ERROR msg => err msg; val _ = Path.expand path handle ERROR msg => err msg; val _ = Context_Position.report ctxt pos (Markup.path (Path.implode_symbolic path)); val _ : Path.T = check_file path handle ERROR msg => err msg; in path end; val check_path = formal_check I; val check_file = formal_check File.check_file; val check_dir = formal_check File.check_dir; fun check_session_dir ctxt opt_dir s = let val dir = Path.expand (check_dir ctxt opt_dir s); val ok = File.is_file (dir + Path.explode("ROOT")) orelse File.is_file (dir + Path.explode("ROOTS")); in if ok then dir else error ("Bad session root directory (missing ROOT or ROOTS): " ^ Path.print dir ^ Position.here (Input.pos_of s)) end; (* antiquotations *) local fun document_antiq (check: Proof.context -> Path.T option -> Input.source -> Path.T) = Args.context -- Scan.lift Parse.path_input >> (fn (ctxt, source) => let val _ = check ctxt NONE source; val latex = Latex.string (Latex.output_ascii_breakable "/" (Input.string_of source)); in Latex.enclose_block "\\isatt{" "}" [latex] end); fun ML_antiq check = Args.context -- Scan.lift Parse.path_input >> (fn (ctxt, source) => check ctxt (SOME Path.current) source |> ML_Syntax.print_path); in val _ = Theory.setup - (Thy_Output.antiquotation_verbatim_embedded \<^binding>\session\ + (Document_Output.antiquotation_verbatim_embedded \<^binding>\session\ (Scan.lift Parse.embedded_position) check_session #> - Thy_Output.antiquotation_raw_embedded \<^binding>\path\ (document_antiq check_path) (K I) #> - Thy_Output.antiquotation_raw_embedded \<^binding>\file\ (document_antiq check_file) (K I) #> - Thy_Output.antiquotation_raw_embedded \<^binding>\dir\ (document_antiq check_dir) (K I) #> + Document_Output.antiquotation_raw_embedded \<^binding>\path\ (document_antiq check_path) (K I) #> + Document_Output.antiquotation_raw_embedded \<^binding>\file\ (document_antiq check_file) (K I) #> + Document_Output.antiquotation_raw_embedded \<^binding>\dir\ (document_antiq check_dir) (K I) #> ML_Antiquotation.value_embedded \<^binding>\path\ (ML_antiq check_path) #> ML_Antiquotation.value_embedded \<^binding>\file\ (ML_antiq check_file) #> ML_Antiquotation.value_embedded \<^binding>\dir\ (ML_antiq check_dir) #> ML_Antiquotation.value_embedded \<^binding>\path_binding\ (Scan.lift (Parse.position Parse.path) >> (ML_Syntax.print_path_binding o Path.explode_binding)) #> ML_Antiquotation.value \<^binding>\master_dir\ (Args.theory >> (ML_Syntax.print_path o master_directory))); end; end; diff --git a/src/Pure/ROOT.ML b/src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML +++ b/src/Pure/ROOT.ML @@ -1,358 +1,358 @@ (* Title: Pure/ROOT.ML Author: Makarius Main entry point for the Isabelle/Pure bootstrap process. Note: When this file is open in the Prover IDE, the ML files of Isabelle/Pure can be explored interactively. This is a separate copy of Pure within Pure: it does not affect the running logic session. *) chapter "Isabelle/Pure bootstrap"; ML_file "ML/ml_name_space.ML"; section "Bootstrap phase 0: Poly/ML setup"; ML_file "ML/ml_init.ML"; ML_file "ML/ml_system.ML"; ML_file "General/basics.ML"; ML_file "General/symbol_explode.ML"; ML_file "Concurrent/multithreading.ML"; ML_file "Concurrent/unsynchronized.ML"; ML_file "Concurrent/synchronized.ML"; ML_file "Concurrent/counter.ML"; ML_file "ML/ml_heap.ML"; ML_file "ML/ml_profiling.ML"; ML_file "ML/ml_print_depth0.ML"; ML_file "ML/ml_pretty.ML"; ML_file "ML/ml_compiler0.ML"; section "Bootstrap phase 1: towards ML within position context"; subsection "Library of general tools"; ML_file "library.ML"; ML_file "General/print_mode.ML"; ML_file "General/alist.ML"; ML_file "General/table.ML"; ML_file "General/random.ML"; ML_file "General/value.ML"; ML_file "General/properties.ML"; ML_file "General/output.ML"; ML_file "PIDE/markup.ML"; ML_file "General/utf8.ML"; ML_file "General/scan.ML"; ML_file "General/source.ML"; ML_file "General/symbol.ML"; ML_file "General/position.ML"; ML_file "General/symbol_pos.ML"; ML_file "General/input.ML"; ML_file "General/comment.ML"; ML_file "General/antiquote.ML"; ML_file "ML/ml_lex.ML"; ML_file "ML/ml_compiler1.ML"; section "Bootstrap phase 2: towards ML within Isar context"; subsection "Library of general tools"; ML_file "General/integer.ML"; ML_file "General/stack.ML"; ML_file "General/queue.ML"; ML_file "General/heap.ML"; ML_file "General/same.ML"; ML_file "General/ord_list.ML"; ML_file "General/balanced_tree.ML"; ML_file "General/linear_set.ML"; ML_file "General/buffer.ML"; ML_file "General/pretty.ML"; ML_file "General/rat.ML"; ML_file "PIDE/xml.ML"; ML_file "General/path.ML"; ML_file "General/url.ML"; ML_file "System/bash.ML"; ML_file "General/file.ML"; ML_file "General/long_name.ML"; ML_file "General/binding.ML"; ML_file "General/socket_io.ML"; ML_file "General/seq.ML"; ML_file "General/time.ML"; ML_file "General/timing.ML"; ML_file "General/sha1.ML"; ML_file "PIDE/yxml.ML"; ML_file "PIDE/byte_message.ML"; ML_file "PIDE/protocol_message.ML"; ML_file "PIDE/document_id.ML"; ML_file "General/change_table.ML"; ML_file "General/graph.ML"; ML_file "System/options.ML"; subsection "Fundamental structures"; ML_file "name.ML"; ML_file "term.ML"; ML_file "context.ML"; ML_file "config.ML"; ML_file "context_position.ML"; ML_file "soft_type_system.ML"; subsection "Concurrency within the ML runtime"; ML_file "ML/exn_properties.ML"; ML_file_no_debug "ML/exn_debugger.ML"; ML_file "Concurrent/thread_data_virtual.ML"; ML_file "Concurrent/isabelle_thread.ML"; ML_file "Concurrent/single_assignment.ML"; ML_file "Concurrent/par_exn.ML"; ML_file "Concurrent/task_queue.ML"; ML_file "Concurrent/future.ML"; ML_file "Concurrent/event_timer.ML"; ML_file "Concurrent/timeout.ML"; ML_file "Concurrent/lazy.ML"; ML_file "Concurrent/par_list.ML"; ML_file "Concurrent/mailbox.ML"; ML_file "Concurrent/cache.ML"; ML_file "PIDE/active.ML"; ML_file "Thy/export.ML"; subsection "Inner syntax"; ML_file "Syntax/type_annotation.ML"; ML_file "Syntax/term_position.ML"; ML_file "Syntax/lexicon.ML"; ML_file "Syntax/ast.ML"; ML_file "Syntax/syntax_ext.ML"; ML_file "Syntax/parser.ML"; ML_file "Syntax/syntax_trans.ML"; ML_file "Syntax/mixfix.ML"; ML_file "Syntax/printer.ML"; ML_file "Syntax/syntax.ML"; subsection "Core of tactical proof system"; ML_file "term_ord.ML"; ML_file "term_subst.ML"; ML_file "General/completion.ML"; ML_file "General/name_space.ML"; ML_file "sorts.ML"; ML_file "type.ML"; ML_file "logic.ML"; ML_file "Syntax/simple_syntax.ML"; ML_file "net.ML"; ML_file "item_net.ML"; ML_file "envir.ML"; ML_file "consts.ML"; ML_file "term_xml.ML"; ML_file "primitive_defs.ML"; ML_file "sign.ML"; ML_file "defs.ML"; ML_file "term_sharing.ML"; ML_file "pattern.ML"; ML_file "unify.ML"; ML_file "theory.ML"; ML_file "proofterm.ML"; ML_file "thm.ML"; ML_file "more_pattern.ML"; ML_file "more_unify.ML"; ML_file "more_thm.ML"; ML_file "facts.ML"; ML_file "thm_name.ML"; ML_file "global_theory.ML"; ML_file "pure_thy.ML"; ML_file "drule.ML"; ML_file "morphism.ML"; ML_file "variable.ML"; ML_file "conv.ML"; ML_file "goal_display.ML"; ML_file "tactical.ML"; ML_file "search.ML"; ML_file "tactic.ML"; ML_file "raw_simplifier.ML"; ML_file "conjunction.ML"; ML_file "assumption.ML"; subsection "Isar -- Intelligible Semi-Automated Reasoning"; (*ML support and global execution*) ML_file "ML/ml_syntax.ML"; ML_file "ML/ml_env.ML"; ML_file "ML/ml_options.ML"; ML_file "ML/ml_print_depth.ML"; ML_file_no_debug "Isar/runtime.ML"; ML_file "PIDE/execution.ML"; ML_file "ML/ml_compiler.ML"; ML_file "skip_proof.ML"; ML_file "goal.ML"; (*outer syntax*) ML_file "Isar/keyword.ML"; ML_file "Isar/token.ML"; ML_file "Isar/parse.ML"; ML_file "Thy/document_source.ML"; ML_file "Thy/thy_header.ML"; ML_file "Thy/document_marker.ML"; (*proof context*) ML_file "Isar/object_logic.ML"; ML_file "Isar/rule_cases.ML"; ML_file "Isar/auto_bind.ML"; ML_file "type_infer.ML"; ML_file "Syntax/local_syntax.ML"; ML_file "Isar/proof_context.ML"; ML_file "type_infer_context.ML"; ML_file "Syntax/syntax_phases.ML"; ML_file "Isar/args.ML"; (*theory specifications*) ML_file "Isar/local_defs.ML"; ML_file "Isar/local_theory.ML"; ML_file "Isar/entity.ML"; ML_file "PIDE/command_span.ML"; ML_file "Thy/thy_element.ML"; ML_file "Thy/markdown.ML"; ML_file "Thy/latex.ML"; (*ML with context and antiquotations*) ML_file "ML/ml_context.ML"; ML_file "ML/ml_antiquotation.ML"; ML_file "ML/ml_compiler2.ML"; ML_file "ML/ml_antiquotations1.ML"; section "Bootstrap phase 3: towards theory Pure and final ML toplevel setup"; (*basic proof engine*) ML_file "par_tactical.ML"; ML_file "context_tactic.ML"; ML_file "Isar/proof_display.ML"; ML_file "Isar/attrib.ML"; ML_file "Isar/context_rules.ML"; ML_file "Isar/method.ML"; ML_file "Isar/proof.ML"; ML_file "Isar/element.ML"; ML_file "Isar/obtain.ML"; ML_file "Isar/subgoal.ML"; ML_file "Isar/calculation.ML"; (*local theories and targets*) ML_file "Isar/locale.ML"; ML_file "Isar/generic_target.ML"; ML_file "Isar/bundle.ML"; ML_file "Isar/overloading.ML"; ML_file "axclass.ML"; ML_file "Isar/class.ML"; ML_file "Isar/named_target.ML"; ML_file "Isar/expression.ML"; ML_file "Isar/interpretation.ML"; ML_file "Isar/class_declaration.ML"; ML_file "Isar/target_context.ML"; ML_file "Isar/experiment.ML"; ML_file "simplifier.ML"; ML_file "Tools/plugin.ML"; (*executable theory content*) ML_file "Isar/code.ML"; (*specifications*) ML_file "Isar/spec_rules.ML"; ML_file "Isar/specification.ML"; ML_file "Isar/parse_spec.ML"; ML_file "Isar/typedecl.ML"; (*toplevel transactions*) ML_file "Isar/proof_node.ML"; ML_file "Isar/toplevel.ML"; (*proof term operations*) ML_file "Proof/proof_rewrite_rules.ML"; ML_file "Proof/proof_syntax.ML"; ML_file "Proof/proof_checker.ML"; ML_file "Proof/extraction.ML"; (*Isabelle system*) ML_file "PIDE/protocol_command.ML"; ML_file "System/scala.ML"; ML_file "System/process_result.ML"; ML_file "System/isabelle_system.ML"; (*theory documents*) ML_file "Thy/term_style.ML"; ML_file "Isar/outer_syntax.ML"; ML_file "ML/ml_antiquotations2.ML"; ML_file "ML/ml_pid.ML"; ML_file "Thy/document_antiquotation.ML"; -ML_file "Thy/thy_output.ML"; +ML_file "Thy/document_output.ML"; ML_file "Thy/document_antiquotations.ML"; ML_file "General/graph_display.ML"; ML_file "pure_syn.ML"; ML_file "PIDE/command.ML"; ML_file "PIDE/query_operation.ML"; ML_file "PIDE/resources.ML"; ML_file "Thy/thy_info.ML"; ML_file "thm_deps.ML"; ML_file "Thy/export_theory.ML"; ML_file "Thy/sessions.ML"; ML_file "PIDE/session.ML"; ML_file "PIDE/document.ML"; (*theory and proof operations*) ML_file "Isar/isar_cmd.ML"; subsection "Isabelle/Isar system"; ML_file "System/command_line.ML"; ML_file "System/message_channel.ML"; ML_file "System/isabelle_process.ML"; ML_file "System/scala_compiler.ML"; ML_file "System/isabelle_tool.ML"; ML_file "Thy/bibtex.ML"; ML_file "PIDE/protocol.ML"; ML_file "General/output_primitives_virtual.ML"; subsection "Miscellaneous tools and packages for Pure Isabelle"; ML_file "ML/ml_pp.ML"; ML_file "ML/ml_thms.ML"; ML_file "ML/ml_file.ML"; ML_file "Tools/build.ML"; ML_file "Tools/named_thms.ML"; ML_file "Tools/print_operation.ML"; ML_file "Tools/rail.ML"; ML_file "Tools/rule_insts.ML"; ML_file "Tools/thy_deps.ML"; ML_file "Tools/class_deps.ML"; ML_file "Tools/find_theorems.ML"; ML_file "Tools/find_consts.ML"; ML_file "Tools/simplifier_trace.ML"; ML_file_no_debug "Tools/debugger.ML"; ML_file "Tools/named_theorems.ML"; ML_file "Tools/doc.ML"; ML_file "Tools/jedit.ML"; ML_file "Tools/ghc.ML"; ML_file "Tools/generated_files.ML" diff --git a/src/Pure/System/isabelle_tool.ML b/src/Pure/System/isabelle_tool.ML --- a/src/Pure/System/isabelle_tool.ML +++ b/src/Pure/System/isabelle_tool.ML @@ -1,44 +1,44 @@ (* Title: Pure/System/isabelle_tool.ML Author: Makarius Support for Isabelle system tools. *) signature ISABELLE_TOOL = sig val isabelle_tools: unit -> (string * Position.T) list val check: Proof.context -> string * Position.T -> string end; structure Isabelle_Tool: ISABELLE_TOOL = struct (* list tools *) fun symbolic_file (a, b) = if a = Markup.fileN then (a, Path.explode b |> Path.implode_symbolic) else (a, b); fun isabelle_tools () = \<^scala>\isabelle_tools\ "" |> YXML.parse_body |> let open XML.Decode in list (pair string properties) end |> map (apsnd (map symbolic_file #> Position.of_properties)); (* check *) fun check ctxt arg = Completion.check_item Markup.toolN (fn (name, pos) => Markup.entity Markup.toolN name |> Markup.properties (Position.def_properties_of pos)) (isabelle_tools ()) ctxt arg; val _ = Theory.setup - (Thy_Output.antiquotation_verbatim_embedded \<^binding>\tool\ + (Document_Output.antiquotation_verbatim_embedded \<^binding>\tool\ (Scan.lift Parse.embedded_position) check); end; diff --git a/src/Pure/System/scala_compiler.ML b/src/Pure/System/scala_compiler.ML --- a/src/Pure/System/scala_compiler.ML +++ b/src/Pure/System/scala_compiler.ML @@ -1,99 +1,99 @@ (* Title: Pure/System/scala_compiler.ML Author: Makarius Scala compiler operations. *) signature SCALA_COMPILER = sig val toplevel: bool -> string -> unit val static_check: string * Position.T -> unit end; structure Scala_Compiler: SCALA_COMPILER = struct (* check declaration *) fun toplevel interpret source = let val errors = (interpret, source) |> let open XML.Encode in pair bool string end |> YXML.string_of_body |> \<^scala>\scala_toplevel\ |> YXML.parse_body |> let open XML.Decode in list string end in if null errors then () else error (cat_lines errors) end; fun static_check (source, pos) = toplevel false ("package test\nclass __Dummy__ { __dummy__ => " ^ source ^ " }") handle ERROR msg => error (msg ^ Position.here pos); (* antiquotations *) local fun make_list bg en = space_implode "," #> enclose bg en; fun print_args [] = "" | print_args xs = make_list "(" ")" xs; fun print_types [] = "" | print_types Ts = make_list "[" "]" Ts; fun print_class (c, Ts) = c ^ print_types Ts; val types = Scan.optional (Parse.$$$ "[" |-- Parse.list1 Parse.name --| Parse.$$$ "]") []; val class = Scan.option (Parse.$$$ "(" |-- Parse.!!! (Parse.$$$ "in" |-- Parse.name -- types --| Parse.$$$ ")")); val arguments = (Parse.nat >> (fn n => replicate n "_") || Parse.list (Parse.underscore || Parse.name >> (fn T => "_ : " ^ T))) >> print_args; val args = Scan.optional (Parse.$$$ "(" |-- arguments --| Parse.$$$ ")") " _"; fun scala_name name = let val latex = Latex.string (Latex.output_ascii_breakable "." name) in Latex.enclose_block "\\isatt{" "}" [latex] end; in val _ = Theory.setup - (Thy_Output.antiquotation_verbatim_embedded \<^binding>\scala\ + (Document_Output.antiquotation_verbatim_embedded \<^binding>\scala\ (Scan.lift Args.embedded_position) (fn _ => fn (s, pos) => (static_check (s, pos); s)) #> - Thy_Output.antiquotation_raw_embedded \<^binding>\scala_type\ + Document_Output.antiquotation_raw_embedded \<^binding>\scala_type\ (Scan.lift (Args.embedded_position -- (types >> print_types))) (fn _ => fn ((t, pos), type_args) => (static_check ("type _Test_" ^ type_args ^ " = " ^ t ^ type_args, pos); scala_name (t ^ type_args))) #> - Thy_Output.antiquotation_raw_embedded \<^binding>\scala_object\ + Document_Output.antiquotation_raw_embedded \<^binding>\scala_object\ (Scan.lift Args.embedded_position) (fn _ => fn (x, pos) => (static_check ("val _test_ = " ^ x, pos); scala_name x)) #> - Thy_Output.antiquotation_raw_embedded \<^binding>\scala_method\ + Document_Output.antiquotation_raw_embedded \<^binding>\scala_method\ (Scan.lift (class -- Args.embedded_position -- types -- args)) (fn _ => fn (((class_context, (method, pos)), method_types), method_args) => let val class_types = (case class_context of SOME (_, Ts) => Ts | NONE => []); val def = "def _test_" ^ print_types (merge (op =) (method_types, class_types)); val def_context = (case class_context of NONE => def ^ " = " | SOME c => def ^ "(_this_ : " ^ print_class c ^ ") = _this_."); val source = def_context ^ method ^ method_args; val _ = static_check (source, pos); val text = (case class_context of NONE => method | SOME c => print_class c ^ "." ^ method); in scala_name text end)); end; end; diff --git a/src/Pure/Thy/bibtex.ML b/src/Pure/Thy/bibtex.ML --- a/src/Pure/Thy/bibtex.ML +++ b/src/Pure/Thy/bibtex.ML @@ -1,66 +1,66 @@ (* Title: Pure/Thy/bibtex.ML Author: Makarius BibTeX support. *) signature BIBTEX = sig val check_database: Position.T -> string -> (string * Position.T) list * (string * Position.T) list val check_database_output: Position.T -> string -> unit val cite_macro: string Config.T end; structure Bibtex: BIBTEX = struct (* check database *) type message = string * Position.T; fun check_database pos0 database = \<^scala>\bibtex_check_database\ database |> YXML.parse_body |> let open XML.Decode in pair (list (pair string properties)) (list (pair string properties)) end |> (apply2 o map o apsnd) (fn pos => Position.of_properties (pos @ Position.get_props pos0)); fun check_database_output pos0 database = let val (errors, warnings) = check_database pos0 database in errors |> List.app (fn (msg, pos) => Output.error_message ("Bibtex error" ^ Position.here pos ^ ":\n " ^ msg)); warnings |> List.app (fn (msg, pos) => warning ("Bibtex warning" ^ Position.here pos ^ ":\n " ^ msg)) end; (* document antiquotations *) val cite_macro = Attrib.setup_config_string \<^binding>\cite_macro\ (K "cite"); val _ = Theory.setup (Document_Antiquotation.setup_option \<^binding>\cite_macro\ (Config.put cite_macro) #> - Thy_Output.antiquotation_raw \<^binding>\cite\ + Document_Output.antiquotation_raw \<^binding>\cite\ (Scan.lift (Scan.option (Parse.verbatim || Parse.cartouche) -- Parse.and_list1 Args.name_position)) (fn ctxt => fn (opt, citations) => let val _ = Context_Position.reports ctxt (map (fn (name, pos) => (pos, Markup.citation name)) citations); val thy_name = Context.theory_long_name (Proof_Context.theory_of ctxt); val bibtex_entries = Resources.theory_bibtex_entries thy_name; val _ = if null bibtex_entries andalso thy_name <> Context.PureN then () else citations |> List.app (fn (name, pos) => if member (op =) bibtex_entries name then () else error ("Unknown Bibtex entry " ^ quote name ^ Position.here pos)); val opt_arg = (case opt of NONE => "" | SOME s => "[" ^ s ^ "]"); val arg = "{" ^ space_implode "," (map #1 citations) ^ "}"; in Latex.string ("\\" ^ Config.get ctxt cite_macro ^ opt_arg ^ arg) end)); end; diff --git a/src/Pure/Thy/document_antiquotations.ML b/src/Pure/Thy/document_antiquotations.ML --- a/src/Pure/Thy/document_antiquotations.ML +++ b/src/Pure/Thy/document_antiquotations.ML @@ -1,401 +1,401 @@ (* Title: Pure/Thy/document_antiquotations.ML Author: Makarius Miscellaneous document antiquotations. *) structure Document_Antiquotations: sig end = struct (* basic entities *) local type style = term -> term; fun pretty_term_style ctxt (style: style, t) = - Thy_Output.pretty_term ctxt (style t); + Document_Output.pretty_term ctxt (style t); fun pretty_thms_style ctxt (style: style, ths) = - map (fn th => Thy_Output.pretty_term ctxt (style (Thm.full_prop_of th))) ths; + map (fn th => Document_Output.pretty_term ctxt (style (Thm.full_prop_of th))) ths; fun pretty_term_typ ctxt (style: style, t) = let val t' = style t - in Thy_Output.pretty_term ctxt (Type.constraint (Term.fastype_of t') t') end; + in Document_Output.pretty_term ctxt (Type.constraint (Term.fastype_of t') t') end; fun pretty_term_typeof ctxt (style: style, t) = Syntax.pretty_typ ctxt (Term.fastype_of (style t)); fun pretty_const ctxt c = let val t = Const (c, Consts.type_scheme (Proof_Context.consts_of ctxt) c) handle TYPE (msg, _, _) => error msg; val (t', _) = yield_singleton (Variable.import_terms true) t ctxt; - in Thy_Output.pretty_term ctxt t' end; + in Document_Output.pretty_term ctxt t' end; fun pretty_abbrev ctxt s = let val t = Syntax.read_term (Proof_Context.set_mode Proof_Context.mode_abbrev ctxt) s; fun err () = error ("Abbreviated constant expected: " ^ Syntax.string_of_term ctxt t); val (head, args) = Term.strip_comb t; val (c, T) = Term.dest_Const head handle TERM _ => err (); val (U, u) = Consts.the_abbreviation (Proof_Context.consts_of ctxt) c handle TYPE _ => err (); val t' = Term.betapplys (Envir.expand_atom T (U, u), args); val eq = Logic.mk_equals (t, t'); val ctxt' = Proof_Context.augment eq ctxt; in Proof_Context.pretty_term_abbrev ctxt' eq end; fun pretty_locale ctxt (name, pos) = let val thy = Proof_Context.theory_of ctxt in Pretty.str (Locale.extern thy (Locale.check thy (name, pos))) end; fun pretty_class ctxt s = Pretty.str (Proof_Context.extern_class ctxt (Proof_Context.read_class ctxt s)); fun pretty_type ctxt s = let val Type (name, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s in Pretty.str (Proof_Context.extern_type ctxt name) end; fun pretty_prf full ctxt = Proof_Syntax.pretty_standard_proof_of ctxt full; fun pretty_theory ctxt (name, pos) = (Theory.check {long = true} ctxt (name, pos); Pretty.str name); -val basic_entity = Thy_Output.antiquotation_pretty_source_embedded; +val basic_entity = Document_Output.antiquotation_pretty_source_embedded; fun basic_entities name scan pretty = Document_Antiquotation.setup name scan (fn {context = ctxt, source = src, argument = xs} => - Thy_Output.pretty_items_source ctxt {embedded = false} src (map (pretty ctxt) xs)); + Document_Output.pretty_items_source ctxt {embedded = false} src (map (pretty ctxt) xs)); val _ = Theory.setup (basic_entity \<^binding>\prop\ (Term_Style.parse -- Args.prop) pretty_term_style #> basic_entity \<^binding>\term\ (Term_Style.parse -- Args.term) pretty_term_style #> basic_entity \<^binding>\term_type\ (Term_Style.parse -- Args.term) pretty_term_typ #> basic_entity \<^binding>\typeof\ (Term_Style.parse -- Args.term) pretty_term_typeof #> basic_entity \<^binding>\const\ (Args.const {proper = true, strict = false}) pretty_const #> basic_entity \<^binding>\abbrev\ (Scan.lift Args.embedded_inner_syntax) pretty_abbrev #> basic_entity \<^binding>\typ\ Args.typ_abbrev Syntax.pretty_typ #> basic_entity \<^binding>\locale\ (Scan.lift Args.embedded_position) pretty_locale #> basic_entity \<^binding>\class\ (Scan.lift Args.embedded_inner_syntax) pretty_class #> basic_entity \<^binding>\type\ (Scan.lift Args.embedded_inner_syntax) pretty_type #> basic_entity \<^binding>\theory\ (Scan.lift Args.embedded_position) pretty_theory #> basic_entities \<^binding>\prf\ Attrib.thms (pretty_prf false) #> basic_entities \<^binding>\full_prf\ Attrib.thms (pretty_prf true) #> Document_Antiquotation.setup \<^binding>\thm\ (Term_Style.parse -- Attrib.thms) (fn {context = ctxt, source = src, argument = arg} => - Thy_Output.pretty_items_source ctxt {embedded = false} src (pretty_thms_style ctxt arg))); + Document_Output.pretty_items_source ctxt {embedded = false} src (pretty_thms_style ctxt arg))); in end; (* Markdown errors *) local fun markdown_error binding = Document_Antiquotation.setup binding (Scan.succeed ()) (fn {source = src, ...} => error ("Bad Markdown structure: illegal " ^ quote (Binding.name_of binding) ^ Position.here (Position.no_range_position (#1 (Token.range_of src))))) val _ = Theory.setup (markdown_error \<^binding>\item\ #> markdown_error \<^binding>\enum\ #> markdown_error \<^binding>\descr\); in end; (* control spacing *) val _ = Theory.setup - (Thy_Output.antiquotation_raw \<^binding>\noindent\ (Scan.succeed ()) + (Document_Output.antiquotation_raw \<^binding>\noindent\ (Scan.succeed ()) (fn _ => fn () => Latex.string "\\noindent") #> - Thy_Output.antiquotation_raw \<^binding>\smallskip\ (Scan.succeed ()) + Document_Output.antiquotation_raw \<^binding>\smallskip\ (Scan.succeed ()) (fn _ => fn () => Latex.string "\\smallskip") #> - Thy_Output.antiquotation_raw \<^binding>\medskip\ (Scan.succeed ()) + Document_Output.antiquotation_raw \<^binding>\medskip\ (Scan.succeed ()) (fn _ => fn () => Latex.string "\\medskip") #> - Thy_Output.antiquotation_raw \<^binding>\bigskip\ (Scan.succeed ()) + Document_Output.antiquotation_raw \<^binding>\bigskip\ (Scan.succeed ()) (fn _ => fn () => Latex.string "\\bigskip")); (* nested document text *) local fun nested_antiquotation name s1 s2 = - Thy_Output.antiquotation_raw_embedded name (Scan.lift Args.cartouche_input) + Document_Output.antiquotation_raw_embedded name (Scan.lift Args.cartouche_input) (fn ctxt => fn txt => - (Context_Position.reports ctxt (Thy_Output.document_reports txt); - Latex.enclose_block s1 s2 (Thy_Output.output_document ctxt {markdown = false} txt))); + (Context_Position.reports ctxt (Document_Output.document_reports txt); + Latex.enclose_block s1 s2 (Document_Output.output_document ctxt {markdown = false} txt))); val _ = Theory.setup (nested_antiquotation \<^binding>\footnote\ "\\footnote{" "}" #> nested_antiquotation \<^binding>\emph\ "\\emph{" "}" #> nested_antiquotation \<^binding>\bold\ "\\textbf{" "}"); in end; (* index entries *) local val strip_symbols = [Symbol.open_, Symbol.close, "'", "\"", "`"]; fun strip_symbol sym = if member (op =) strip_symbols sym then "" else (case Symbol.decode sym of Symbol.Char s => s | Symbol.UTF8 s => s | Symbol.Sym s => s | Symbol.Control s => s | _ => ""); fun strip_antiq _ (Antiquote.Text body) = map Symbol_Pos.symbol body | strip_antiq _ (Antiquote.Control {body, ...}) = map Symbol_Pos.symbol body | strip_antiq ctxt (Antiquote.Antiq antiq) = Document_Antiquotation.read_antiq ctxt antiq |> #2 |> tl |> maps (Symbol.explode o Token.content_of); in fun clean_text ctxt txt = let val pos = Input.pos_of txt; val syms = Input.source_explode txt; val ants = Antiquote.parse_comments pos (trim (Symbol.is_blank o Symbol_Pos.symbol) syms); in ants |> maps (strip_antiq ctxt) |> map strip_symbol |> implode end; end; local val index_like = Parse.$$$ "(" |-- Parse.!!! (Parse.$$$ "is" |-- Args.name --| Parse.$$$ ")"); val index_args = Parse.enum1 "!" (Args.embedded_input -- Scan.option index_like); -fun output_text ctxt = Latex.block o Thy_Output.output_document ctxt {markdown = false}; +fun output_text ctxt = Latex.block o Document_Output.output_document ctxt {markdown = false}; fun index binding def = - Thy_Output.antiquotation_raw binding (Scan.lift index_args) + Document_Output.antiquotation_raw binding (Scan.lift index_args) (fn ctxt => fn args => let - val _ = Context_Position.reports ctxt (maps (Thy_Output.document_reports o #1) args); + val _ = Context_Position.reports ctxt (maps (Document_Output.document_reports o #1) args); fun make_item (txt, opt_like) = let val text = output_text ctxt txt; val like = (case opt_like of SOME s => s | NONE => clean_text ctxt txt); val _ = if is_none opt_like andalso Context_Position.is_visible ctxt then writeln ("(" ^ Markup.markup Markup.keyword2 "is" ^ " " ^ quote like ^ ")" ^ Position.here (Input.pos_of txt)) else (); in {text = text, like = like} end; in Latex.index_entry {items = map make_item args, def = def} end); val _ = Theory.setup (index \<^binding>\index_ref\ false #> index \<^binding>\index_def\ true); in end; (* quasi-formal text (unchecked) *) local fun report_text ctxt text = let val pos = Input.pos_of text in Context_Position.reports ctxt [(pos, Markup.language_text (Input.is_delimited text)), (pos, Markup.raw_text)] end; fun prepare_text ctxt = Input.source_content #> #1 #> Document_Antiquotation.prepare_lines ctxt; fun text_antiquotation name = - Thy_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input) + Document_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input) (fn ctxt => fn text => let val _ = report_text ctxt text; in prepare_text ctxt text - |> Thy_Output.output_source ctxt - |> Thy_Output.isabelle ctxt + |> Document_Output.output_source ctxt + |> Document_Output.isabelle ctxt end); val theory_text_antiquotation = - Thy_Output.antiquotation_raw_embedded \<^binding>\theory_text\ (Scan.lift Args.text_input) + Document_Output.antiquotation_raw_embedded \<^binding>\theory_text\ (Scan.lift Args.text_input) (fn ctxt => fn text => let val keywords = Thy_Header.get_keywords' ctxt; val _ = report_text ctxt text; val _ = Input.source_explode text |> Token.tokenize keywords {strict = true} |> maps (Token.reports keywords) |> Context_Position.reports_text ctxt; in prepare_text ctxt text |> Token.explode0 keywords - |> maps (Thy_Output.output_token ctxt) - |> Thy_Output.isabelle ctxt + |> maps (Document_Output.output_token ctxt) + |> Document_Output.isabelle ctxt end); val _ = Theory.setup (text_antiquotation \<^binding>\text\ #> text_antiquotation \<^binding>\cartouche\ #> theory_text_antiquotation); in end; (* goal state *) local fun goal_state name main = - Thy_Output.antiquotation_pretty name (Scan.succeed ()) + Document_Output.antiquotation_pretty name (Scan.succeed ()) (fn ctxt => fn () => Goal_Display.pretty_goal (Config.put Goal_Display.show_main_goal main ctxt) (#goal (Proof.goal (Toplevel.proof_of (Toplevel.presentation_state ctxt))))); val _ = Theory.setup (goal_state \<^binding>\goals\ true #> goal_state \<^binding>\subgoals\ false); in end; (* embedded lemma *) val _ = Theory.setup (Document_Antiquotation.setup \<^binding>\lemma\ (Scan.lift (Scan.ahead Parse.not_eof) -- Args.prop -- Scan.lift (Parse.position (Parse.reserved "by") -- Method.parse -- Scan.option Method.parse)) (fn {context = ctxt, source = src, argument = ((prop_tok, prop), (((_, by_pos), m1), m2))} => let val reports = (by_pos, Markup.keyword1 |> Markup.keyword_properties) :: maps Method.reports_of (m1 :: the_list m2); val _ = Context_Position.reports ctxt reports; (* FIXME check proof!? *) val _ = ctxt |> Proof.theorem NONE (K I) [[(prop, [])]] |> Proof.global_terminal_proof (m1, m2); in - Thy_Output.pretty_source ctxt {embedded = false} - [hd src, prop_tok] (Thy_Output.pretty_term ctxt prop) + Document_Output.pretty_source ctxt {embedded = false} + [hd src, prop_tok] (Document_Output.pretty_term ctxt prop) end)); (* verbatim text *) val _ = Theory.setup - (Thy_Output.antiquotation_verbatim_embedded \<^binding>\verbatim\ (Scan.lift Args.text_input) + (Document_Output.antiquotation_verbatim_embedded \<^binding>\verbatim\ (Scan.lift Args.text_input) (fn ctxt => fn text => let val pos = Input.pos_of text; val _ = Context_Position.reports ctxt [(pos, Markup.language_verbatim (Input.is_delimited text)), (pos, Markup.raw_text)]; in #1 (Input.source_content text) end)); (* bash functions *) val _ = Theory.setup - (Thy_Output.antiquotation_verbatim_embedded \<^binding>\bash_function\ + (Document_Output.antiquotation_verbatim_embedded \<^binding>\bash_function\ (Scan.lift Args.embedded_position) Isabelle_System.check_bash_function); (* system options *) val _ = Theory.setup - (Thy_Output.antiquotation_verbatim_embedded \<^binding>\system_option\ + (Document_Output.antiquotation_verbatim_embedded \<^binding>\system_option\ (Scan.lift Args.embedded_position) (fn ctxt => fn (name, pos) => let val _ = Completion.check_option (Options.default ()) ctxt (name, pos); in name end)); (* ML text *) local fun ml_text name ml = - Thy_Output.antiquotation_verbatim_embedded name (Scan.lift Args.text_input) + Document_Output.antiquotation_verbatim_embedded name (Scan.lift Args.text_input) (fn ctxt => fn text => let val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of text) (ml text) in #1 (Input.source_content text) end); fun ml_enclose bg en source = ML_Lex.read bg @ ML_Lex.read_source source @ ML_Lex.read en; val _ = Theory.setup (ml_text \<^binding>\ML\ (ml_enclose "fn _ => (" ");") #> ml_text \<^binding>\ML_op\ (ml_enclose "fn _ => (op " ");") #> ml_text \<^binding>\ML_type\ (ml_enclose "val _ = NONE : (" ") option;") #> ml_text \<^binding>\ML_structure\ (ml_enclose "functor XXX() = struct structure XX = " " end;") #> ml_text \<^binding>\ML_functor\ (* FIXME formal treatment of functor name (!?) *) (fn source => ML_Lex.read ("ML_Env.check_functor " ^ ML_Syntax.print_string (#1 (Input.source_content source)))) #> ml_text \<^binding>\ML_text\ (K [])); in end; (* URLs *) val escape_url = translate_string (fn c => if c = "%" orelse c = "#" orelse c = "^" then "\\" ^ c else c); val _ = Theory.setup - (Thy_Output.antiquotation_raw_embedded \<^binding>\url\ (Scan.lift Args.embedded_input) + (Document_Output.antiquotation_raw_embedded \<^binding>\url\ (Scan.lift Args.embedded_input) (fn ctxt => fn source => let val url = Input.string_of source; val pos = Input.pos_of source; val delimited = Input.is_delimited source; val _ = Context_Position.reports ctxt [(pos, Markup.language_url delimited), (pos, Markup.url url)]; in Latex.enclose_block "\\url{" "}" [Latex.string (escape_url url)] end)); (* formal entities *) local fun entity_antiquotation name check bg en = - Thy_Output.antiquotation_raw name (Scan.lift Args.name_position) + Document_Output.antiquotation_raw name (Scan.lift Args.name_position) (fn ctxt => fn (name, pos) => let val _ = check ctxt (name, pos) in Latex.enclose_block bg en [Latex.string (Output.output name)] end); val _ = Theory.setup (entity_antiquotation \<^binding>\command\ Outer_Syntax.check_command "\\isacommand{" "}" #> entity_antiquotation \<^binding>\method\ Method.check_name "\\isa{" "}" #> entity_antiquotation \<^binding>\attribute\ Attrib.check_name "\\isa{" "}"); in end; end; diff --git a/src/Pure/Thy/thy_output.ML b/src/Pure/Thy/document_output.ML rename from src/Pure/Thy/thy_output.ML rename to src/Pure/Thy/document_output.ML --- a/src/Pure/Thy/thy_output.ML +++ b/src/Pure/Thy/document_output.ML @@ -1,577 +1,577 @@ -(* Title: Pure/Thy/thy_output.ML +(* Title: Pure/Thy/document_output.ML Author: Makarius Theory document output. *) -signature THY_OUTPUT = +signature DOCUMENT_OUTPUT = sig val document_reports: Input.source -> Position.report list val output_document: Proof.context -> {markdown: bool} -> Input.source -> Latex.text list val check_comments: Proof.context -> Symbol_Pos.T list -> unit val output_token: Proof.context -> Token.T -> Latex.text list val output_source: Proof.context -> string -> Latex.text list type segment = {span: Command_Span.span, command: Toplevel.transition, prev_state: Toplevel.state, state: Toplevel.state} val present_thy: Options.T -> theory -> segment list -> Latex.text list val pretty_term: Proof.context -> term -> Pretty.T val pretty_thm: Proof.context -> thm -> Pretty.T val lines: Latex.text list -> Latex.text list val items: Latex.text list -> Latex.text list val isabelle: Proof.context -> Latex.text list -> Latex.text val isabelle_typewriter: Proof.context -> Latex.text list -> Latex.text val typewriter: Proof.context -> string -> Latex.text val verbatim: Proof.context -> string -> Latex.text val source: Proof.context -> {embedded: bool} -> Token.src -> Latex.text val pretty: Proof.context -> Pretty.T -> Latex.text val pretty_source: Proof.context -> {embedded: bool} -> Token.src -> Pretty.T -> Latex.text val pretty_items: Proof.context -> Pretty.T list -> Latex.text val pretty_items_source: Proof.context -> {embedded: bool} -> Token.src -> Pretty.T list -> Latex.text val antiquotation_pretty: binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory val antiquotation_pretty_embedded: binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory val antiquotation_pretty_source: binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory val antiquotation_pretty_source_embedded: binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory val antiquotation_raw: binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory val antiquotation_raw_embedded: binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory val antiquotation_verbatim: binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory val antiquotation_verbatim_embedded: binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory end; -structure Thy_Output: THY_OUTPUT = +structure Document_Output: DOCUMENT_OUTPUT = struct (* output document source *) fun document_reports txt = let val pos = Input.pos_of txt in [(pos, Markup.language_document (Input.is_delimited txt)), (pos, Markup.plain_text)] end; val output_symbols = single o Latex.symbols_output; fun output_comment ctxt (kind, syms) = (case kind of Comment.Comment => Input.cartouche_content syms |> output_document (ctxt |> Config.put Document_Antiquotation.thy_output_display false) {markdown = false} |> Latex.enclose_body "%\n\\isamarkupcmt{" "%\n}" | Comment.Cancel => Symbol_Pos.cartouche_content syms |> output_symbols |> Latex.enclose_body "%\n\\isamarkupcancel{" "}" | Comment.Latex => [Latex.symbols (Symbol_Pos.cartouche_content syms)] | Comment.Marker => []) and output_comment_document ctxt (comment, syms) = (case comment of SOME kind => output_comment ctxt (kind, syms) | NONE => [Latex.symbols syms]) and output_document_text ctxt syms = Comment.read_body syms |> maps (output_comment_document ctxt) and output_document ctxt {markdown} source = let val pos = Input.pos_of source; val syms = Input.source_explode source; val output_antiquotes = maps (Document_Antiquotation.evaluate (output_document_text ctxt) ctxt); fun output_line line = (if Markdown.line_is_item line then [Latex.string "\\item "] else []) @ output_antiquotes (Markdown.line_content line); fun output_block (Markdown.Par lines) = Latex.block (separate (Latex.string "\n") (map (Latex.block o output_line) lines)) | output_block (Markdown.List {kind, body, ...}) = Latex.environment_block (Markdown.print_kind kind) (output_blocks body) and output_blocks blocks = separate (Latex.string "\n\n") (map output_block blocks); in if Toplevel.is_skipped_proof (Toplevel.presentation_state ctxt) then [] else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms then let val ants = Antiquote.parse_comments pos syms; val reports = Antiquote.antiq_reports ants; val blocks = Markdown.read_antiquotes ants; val _ = Context_Position.reports ctxt (reports @ Markdown.reports blocks); in output_blocks blocks end else let val ants = Antiquote.parse_comments pos (trim (Symbol.is_blank o Symbol_Pos.symbol) syms); val reports = Antiquote.antiq_reports ants; val _ = Context_Position.reports ctxt (reports @ Markdown.text_reports ants); in output_antiquotes ants end end; (* output tokens with formal comments *) local val output_symbols_antiq = (fn Antiquote.Text syms => output_symbols syms | Antiquote.Control {name = (name, _), body, ...} => Latex.string (Latex.output_symbols [Symbol.encode (Symbol.Control name)]) :: output_symbols body | Antiquote.Antiq {body, ...} => Latex.enclose_body "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n" (output_symbols body)); fun output_comment_symbols ctxt {antiq} (comment, syms) = (case (comment, antiq) of (NONE, false) => output_symbols syms | (NONE, true) => Antiquote.parse_comments (#1 (Symbol_Pos.range syms)) syms |> maps output_symbols_antiq | (SOME comment, _) => output_comment ctxt (comment, syms)); fun output_body ctxt antiq bg en syms = Comment.read_body syms |> maps (output_comment_symbols ctxt {antiq = antiq}) |> Latex.enclose_body bg en; in fun output_token ctxt tok = let fun output antiq bg en = output_body ctxt antiq bg en (Input.source_explode (Token.input_of tok)); in (case Token.kind_of tok of Token.Comment NONE => [] | Token.Comment (SOME Comment.Marker) => [] | Token.Command => output false "\\isacommand{" "}" | Token.Keyword => if Symbol.is_ascii_identifier (Token.content_of tok) then output false "\\isakeyword{" "}" else output false "" "" | Token.String => output false "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" | Token.Alt_String => output false "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" | Token.Verbatim => output true "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" | Token.Cartouche => output false "{\\isacartoucheopen}" "{\\isacartoucheclose}" | _ => output false "" "") end handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok)); fun output_source ctxt s = output_body ctxt false "" "" (Symbol_Pos.explode (s, Position.none)); fun check_comments ctxt = Comment.read_body #> List.app (fn (comment, syms) => let val pos = #1 (Symbol_Pos.range syms); val _ = comment |> Option.app (fn kind => Context_Position.reports ctxt (map (pair pos) (Comment.kind_markups kind))); val _ = output_comment_symbols ctxt {antiq = false} (comment, syms); in if comment = SOME Comment.Comment then check_comments ctxt syms else () end); end; (** present theory source **) (* presentation tokens *) datatype token = Ignore | Token of Token.T | Heading of string * Input.source | Body of string * Input.source | Raw of Input.source; fun token_with pred (Token tok) = pred tok | token_with _ _ = false; val white_token = token_with Document_Source.is_white; val white_comment_token = token_with Document_Source.is_white_comment; val blank_token = token_with Token.is_blank; val newline_token = token_with Token.is_newline; fun present_token ctxt tok = (case tok of Ignore => [] | Token tok => output_token ctxt tok | Heading (cmd, source) => Latex.enclose_body ("%\n\\isamarkup" ^ cmd ^ "{") "%\n}\n" (output_document ctxt {markdown = false} source) | Body (cmd, source) => [Latex.environment_block ("isamarkup" ^ cmd) (output_document ctxt {markdown = true} source)] | Raw source => Latex.string "%\n" :: output_document ctxt {markdown = true} source @ [Latex.string "\n"]); (* command spans *) type command = string * Position.T; (*name, position*) type source = (token * (string * int)) list; (*token, markup flag, meta-comment depth*) datatype span = Span of command * (source * source * source * source) * bool; fun make_span cmd src = let fun chop_newline (tok :: toks) = if newline_token (fst tok) then ([tok], toks, true) else ([], tok :: toks, false) | chop_newline [] = ([], [], false); val (((src_prefix, src_main), src_suffix1), (src_suffix2, src_appendix, newline)) = src |> chop_prefix (white_token o fst) ||>> chop_suffix (white_token o fst) ||>> chop_prefix (white_comment_token o fst) ||> chop_newline; in Span (cmd, (src_prefix, src_main, src_suffix1 @ src_suffix2, src_appendix), newline) end; (* present spans *) local fun err_bad_nesting here = error ("Bad nesting of commands in presentation" ^ here); fun edge which f (x: string option, y) = if x = y then I else (case which (x, y) of NONE => I | SOME txt => cons (Latex.string (f txt))); val begin_tag = edge #2 Latex.begin_tag; val end_tag = edge #1 Latex.end_tag; fun open_delim delim e = edge #2 Latex.begin_delim e #> delim #> edge #2 Latex.end_delim e; fun close_delim delim e = edge #1 Latex.begin_delim e #> delim #> edge #1 Latex.end_delim e; fun document_tag cmd_pos state state' tagging_stack = let val ctxt' = Toplevel.presentation_context state'; val nesting = Toplevel.level state' - Toplevel.level state; val (tagging, taggings) = tagging_stack; val (tag', tagging') = Document_Source.update_tagging ctxt' tagging; val tagging_stack' = if nesting = 0 andalso not (Toplevel.is_proof state) then tagging_stack else if nesting >= 0 then (tagging', replicate nesting tagging @ taggings) else (case drop (~ nesting - 1) taggings of tg :: tgs => (tg, tgs) | [] => err_bad_nesting (Position.here cmd_pos)); in (tag', tagging_stack') end; fun read_tag s = (case space_explode "%" s of ["", b] => (SOME b, NONE) | [a, b] => (NONE, SOME (a, b)) | _ => error ("Bad document_tags specification: " ^ quote s)); in fun make_command_tag options keywords = let val document_tags = map read_tag (space_explode "," (Options.string options \<^system_option>\document_tags\)); val document_tags_default = map_filter #1 document_tags; val document_tags_command = map_filter #2 document_tags; in fn cmd_name => fn state => fn state' => fn active_tag => let val keyword_tags = if cmd_name = "end" andalso Toplevel.is_end_theory state' then ["theory"] else Keyword.command_tags keywords cmd_name; val command_tags = the_list (AList.lookup (op =) document_tags_command cmd_name) @ keyword_tags @ document_tags_default; val active_tag' = (case command_tags of default_tag :: _ => SOME default_tag | [] => if Keyword.is_vacuous keywords cmd_name andalso Toplevel.is_proof state then active_tag else NONE); in active_tag' end end; fun present_span command_tag span state state' (tagging_stack, active_tag, newline, latex, present_cont) = let val ctxt' = Toplevel.presentation_context state'; val present = fold (fn (tok, (flag, 0)) => fold cons (present_token ctxt' tok) #> cons (Latex.string flag) | _ => I); val Span ((cmd_name, cmd_pos), srcs, span_newline) = span; val (tag', tagging_stack') = document_tag cmd_pos state state' tagging_stack; val active_tag' = if is_some tag' then Option.map #1 tag' else command_tag cmd_name state state' active_tag; val edge = (active_tag, active_tag'); val newline' = if is_none active_tag' then span_newline else newline; val latex' = latex |> end_tag edge |> close_delim (fst present_cont) edge |> snd present_cont |> open_delim (present (#1 srcs)) edge |> begin_tag edge |> present (#2 srcs); val present_cont' = if newline then (present (#3 srcs), present (#4 srcs)) else (I, present (#3 srcs) #> present (#4 srcs)); in (tagging_stack', active_tag', newline', latex', present_cont') end; fun present_trailer ((_, tags), active_tag, _, latex, present_cont) = if not (null tags) then err_bad_nesting " at end of theory" else latex |> end_tag (active_tag, NONE) |> close_delim (fst present_cont) (active_tag, NONE) |> snd present_cont; end; (* present_thy *) local val markup_true = "\\isamarkuptrue%\n"; val markup_false = "\\isamarkupfalse%\n"; val opt_newline = Scan.option (Scan.one Token.is_newline); val ignore = Scan.depend (fn d => opt_newline |-- Scan.one Token.is_begin_ignore >> pair (d + 1)) || Scan.depend (fn d => Scan.one Token.is_end_ignore --| (if d = 0 then Scan.fail_with (K (fn () => "Bad nesting of meta-comments")) else opt_newline) >> pair (d - 1)); val locale = Scan.option ((Parse.$$$ "(" -- Document_Source.improper -- Parse.$$$ "in") |-- Parse.!!! (Document_Source.improper |-- Parse.name --| (Document_Source.improper -- Parse.$$$ ")"))); in type segment = {span: Command_Span.span, command: Toplevel.transition, prev_state: Toplevel.state, state: Toplevel.state}; fun present_thy options thy (segments: segment list) = let val keywords = Thy_Header.get_keywords thy; (* tokens *) val ignored = Scan.state --| ignore >> (fn d => (NONE, (Ignore, ("", d)))); fun markup pred mk flag = Scan.peek (fn d => Document_Source.improper |-- Parse.position (Scan.one (fn tok => Token.is_command tok andalso pred keywords (Token.content_of tok))) -- (Document_Source.annotation |-- Parse.!!!! ((Document_Source.improper -- locale -- Document_Source.improper) |-- Parse.document_source --| Document_Source.improper_end)) >> (fn ((tok, pos'), source) => let val name = Token.content_of tok in (SOME (name, pos'), (mk (name, source), (flag, d))) end)); val command = Scan.peek (fn d => Scan.optional (Scan.one Token.is_command_modifier ::: Document_Source.improper) [] -- Scan.one Token.is_command --| Document_Source.annotation >> (fn (cmd_mod, cmd) => map (fn tok => (NONE, (Token tok, ("", d)))) cmd_mod @ [(SOME (Token.content_of cmd, Token.pos_of cmd), (Token cmd, (markup_false, d)))])); val cmt = Scan.peek (fn d => Scan.one Document_Source.is_black_comment >> (fn tok => (NONE, (Token tok, ("", d))))); val other = Scan.peek (fn d => Parse.not_eof >> (fn tok => (NONE, (Token tok, ("", d))))); val tokens = (ignored || markup Keyword.is_document_heading Heading markup_true || markup Keyword.is_document_body Body markup_true || markup Keyword.is_document_raw (Raw o #2) "") >> single || command || (cmt || other) >> single; (* spans *) val is_eof = fn (_, (Token x, _)) => Token.is_eof x | _ => false; val stopper = Scan.stopper (K (NONE, (Token Token.eof, ("", 0)))) is_eof; val cmd = Scan.one (is_some o fst); val non_cmd = Scan.one (is_none o fst andf not o is_eof) >> #2; val white_comments = Scan.many (white_comment_token o fst o snd); val blank = Scan.one (blank_token o fst o snd); val newline = Scan.one (newline_token o fst o snd); val before_cmd = Scan.option (newline -- white_comments) -- Scan.option (newline -- white_comments) -- Scan.option (blank -- white_comments) -- cmd; val span = Scan.repeat non_cmd -- cmd -- Scan.repeat (Scan.unless before_cmd non_cmd) -- Scan.option (newline >> (single o snd)) >> (fn (((toks1, (cmd, tok2)), toks3), tok4) => make_span (the cmd) (toks1 @ (tok2 :: (toks3 @ the_default [] tok4)))); val spans = segments |> maps (Command_Span.content o #span) |> drop_suffix Token.is_space |> Source.of_list |> Source.source' 0 Token.stopper (Scan.error (Scan.bulk tokens >> flat)) |> Source.source stopper (Scan.error (Scan.bulk span)) |> Source.exhaust; val command_results = segments |> map_filter (fn {command, state, ...} => if Toplevel.is_ignored command then NONE else SOME (command, state)); (* present commands *) val command_tag = make_command_tag options keywords; fun present_command tr span st st' = Toplevel.setmp_thread_position tr (present_span command_tag span st st'); fun present _ [] = I | present st ((span, (tr, st')) :: rest) = present_command tr span st st' #> present st' rest; in if length command_results = length spans then (([], []), NONE, true, [], (I, I)) |> present (Toplevel.init_toplevel ()) (spans ~~ command_results) |> present_trailer |> rev else error "Messed-up outer syntax for presentation" end; end; (** standard output operations **) (* pretty printing *) fun pretty_term ctxt t = Syntax.pretty_term (Proof_Context.augment t ctxt) t; fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of; (* default output *) val lines = separate (Latex.string "\\isanewline%\n"); val items = separate (Latex.string "\\isasep\\isanewline%\n"); fun isabelle ctxt body = if Config.get ctxt Document_Antiquotation.thy_output_display then Latex.environment_block "isabelle" body else Latex.block (Latex.enclose_body "\\isa{" "}" body); fun isabelle_typewriter ctxt body = if Config.get ctxt Document_Antiquotation.thy_output_display then Latex.environment_block "isabellett" body else Latex.block (Latex.enclose_body "\\isatt{" "}" body); fun typewriter ctxt s = isabelle_typewriter ctxt [Latex.string (Latex.output_ascii s)]; fun verbatim ctxt = if Config.get ctxt Document_Antiquotation.thy_output_display then Document_Antiquotation.indent_lines ctxt #> typewriter ctxt else split_lines #> map (typewriter ctxt) #> lines #> Latex.block; fun token_source ctxt {embedded} tok = if Token.is_kind Token.Cartouche tok andalso embedded andalso not (Config.get ctxt Document_Antiquotation.thy_output_source_cartouche) then Token.content_of tok else Token.unparse tok; fun is_source ctxt = Config.get ctxt Document_Antiquotation.thy_output_source orelse Config.get ctxt Document_Antiquotation.thy_output_source_cartouche; fun source ctxt embedded = Token.args_of_src #> map (token_source ctxt embedded #> Document_Antiquotation.prepare_lines ctxt) #> space_implode " " #> output_source ctxt #> isabelle ctxt; fun pretty ctxt = Document_Antiquotation.output ctxt #> Latex.string #> single #> isabelle ctxt; fun pretty_source ctxt embedded src prt = if is_source ctxt then source ctxt embedded src else pretty ctxt prt; fun pretty_items ctxt = map (Document_Antiquotation.output ctxt #> Latex.string) #> items #> isabelle ctxt; fun pretty_items_source ctxt embedded src prts = if is_source ctxt then source ctxt embedded src else pretty_items ctxt prts; (* antiquotation variants *) local fun gen_setup name embedded = if embedded then Document_Antiquotation.setup_embedded name else Document_Antiquotation.setup name; fun gen_antiquotation_pretty name embedded scan f = gen_setup name embedded scan (fn {context = ctxt, argument = x, ...} => pretty ctxt (f ctxt x)); fun gen_antiquotation_pretty_source name embedded scan f = gen_setup name embedded scan (fn {context = ctxt, source = src, argument = x} => pretty_source ctxt {embedded = embedded} src (f ctxt x)); fun gen_antiquotation_raw name embedded scan f = gen_setup name embedded scan (fn {context = ctxt, argument = x, ...} => f ctxt x); fun gen_antiquotation_verbatim name embedded scan f = gen_antiquotation_raw name embedded scan (fn ctxt => verbatim ctxt o f ctxt); in fun antiquotation_pretty name = gen_antiquotation_pretty name false; fun antiquotation_pretty_embedded name = gen_antiquotation_pretty name true; fun antiquotation_pretty_source name = gen_antiquotation_pretty_source name false; fun antiquotation_pretty_source_embedded name = gen_antiquotation_pretty_source name true; fun antiquotation_raw name = gen_antiquotation_raw name false; fun antiquotation_raw_embedded name = gen_antiquotation_raw name true; fun antiquotation_verbatim name = gen_antiquotation_verbatim name false; fun antiquotation_verbatim_embedded name = gen_antiquotation_verbatim name true; end; end; diff --git a/src/Pure/Thy/thy_info.ML b/src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML +++ b/src/Pure/Thy/thy_info.ML @@ -1,483 +1,483 @@ (* Title: Pure/Thy/thy_info.ML Author: Makarius Global theory info database, with auto-loading according to theory and file dependencies, and presentation of theory documents. *) signature THY_INFO = sig type presentation_context = {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T, - segments: Thy_Output.segment list} + segments: Document_Output.segment list} val adjust_pos_properties: presentation_context -> Position.T -> Properties.T val apply_presentation: presentation_context -> theory -> unit val add_presentation: (presentation_context -> theory -> unit) -> theory -> theory val get_names: unit -> string list val lookup_theory: string -> theory option val get_theory: string -> theory val master_directory: string -> Path.T val remove_thy: string -> unit val use_theories: Options.T -> string -> (string * Position.T) list -> unit val use_thy: string -> unit val script_thy: Position.T -> string -> theory -> theory val register_thy: theory -> unit val finish: unit -> unit end; structure Thy_Info: THY_INFO = struct (** theory presentation **) (* artefact names *) fun document_name ext thy = Path.explode_binding0 ("document/" ^ Context.theory_name thy ^ "." ^ ext); val document_tex_name = document_name "tex"; (* hook for consolidated theory *) type presentation_context = {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T, - segments: Thy_Output.segment list}; + segments: Document_Output.segment list}; fun adjust_pos_properties (context: presentation_context) pos = Position.offset_properties_of (#adjust_pos context pos) @ Position.id_properties_of pos; structure Presentation = Theory_Data ( type T = ((presentation_context -> theory -> unit) * stamp) list; val empty = []; val extend = I; fun merge data : T = Library.merge (eq_snd op =) data; ); fun sequential_presentation options = not (Options.bool options \<^system_option>\parallel_presentation\); fun apply_presentation (context: presentation_context) thy = Par_List.map' {name = "apply_presentation", sequential = sequential_presentation (#options context)} (fn (f, _) => f context thy) (Presentation.get thy) |> ignore; fun add_presentation f = Presentation.map (cons (f, stamp ())); val _ = Theory.setup (add_presentation (fn {options, file_pos, segments, ...} => fn thy => if exists (Toplevel.is_skipped_proof o #state) segments then () else let - val body = Thy_Output.present_thy options thy segments; + val body = Document_Output.present_thy options thy segments; in if Options.string options "document" = "false" then () else let val thy_name = Context.theory_name thy; val document_tex_name = document_tex_name thy; val latex = Latex.isabelle_body thy_name body; val output = [Latex.output_text latex, Latex.output_positions file_pos latex]; in Export.export thy document_tex_name (XML.blob output) end end)); (** thy database **) (* messages *) val show_path = space_implode " via " o map quote; fun cycle_msg names = "Cyclic dependency of " ^ show_path names; (* derived graph operations *) fun add_deps name parents G = String_Graph.add_deps_acyclic (name, parents) G handle String_Graph.CYCLES namess => error (cat_lines (map cycle_msg namess)); fun new_entry name parents entry = String_Graph.new_node (name, entry) #> add_deps name parents; (* global thys *) type deps = {master: (Path.T * SHA1.digest), (*master dependencies for thy file*) imports: (string * Position.T) list}; (*source specification of imports (partially qualified)*) fun make_deps master imports : deps = {master = master, imports = imports}; fun master_dir_deps (d: deps option) = the_default Path.current (Option.map (Path.dir o #1 o #master) d); local val global_thys = Synchronized.var "Thy_Info.thys" (String_Graph.empty: (deps option * theory option) String_Graph.T); in fun get_thys () = Synchronized.value global_thys; fun change_thys f = Synchronized.change global_thys f; end; fun get_names () = String_Graph.topological_order (get_thys ()); (* access thy *) fun lookup thys name = try (String_Graph.get_node thys) name; fun lookup_thy name = lookup (get_thys ()) name; fun get thys name = (case lookup thys name of SOME thy => thy | NONE => error ("Theory loader: nothing known about theory " ^ quote name)); fun get_thy name = get (get_thys ()) name; (* access deps *) val lookup_deps = Option.map #1 o lookup_thy; val master_directory = master_dir_deps o #1 o get_thy; (* access theory *) fun lookup_theory name = (case lookup_thy name of SOME (_, SOME theory) => SOME theory | _ => NONE); fun get_theory name = (case lookup_theory name of SOME theory => theory | _ => error ("Theory loader: undefined entry for theory " ^ quote name)); val get_imports = Resources.imports_of o get_theory; (** thy operations **) (* remove *) fun remove name thys = (case lookup thys name of NONE => thys | SOME (NONE, _) => error ("Cannot update finished theory " ^ quote name) | SOME _ => let val succs = String_Graph.all_succs thys [name]; val _ = writeln ("Theory loader: removing " ^ commas_quote succs); in fold String_Graph.del_node succs thys end); val remove_thy = change_thys o remove; (* update *) fun update deps theory thys = let val name = Context.theory_long_name theory; val parents = map Context.theory_long_name (Theory.parents_of theory); val thys' = remove name thys; val _ = map (get thys') parents; in new_entry name parents (SOME deps, SOME theory) thys' end; fun update_thy deps theory = change_thys (update deps theory); (* scheduling loader tasks *) datatype result = Result of {theory: theory, exec_id: Document_ID.exec, present: unit -> unit, commit: unit -> unit, weight: int}; fun theory_result theory = Result {theory = theory, exec_id = Document_ID.none, present = I, commit = I, weight = 0}; fun result_theory (Result {theory, ...}) = theory; fun result_present (Result {present, ...}) = present; fun result_commit (Result {commit, ...}) = commit; fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i); fun join_theory (Result {theory, exec_id, ...}) = let val _ = Execution.join [exec_id]; val res = Exn.capture Thm.consolidate_theory theory; val exns = maps Task_Queue.group_status (Execution.peek exec_id); in res :: map Exn.Exn exns end; datatype task = Task of string list * (theory list -> result) | Finished of theory; fun task_finished (Task _) = false | task_finished (Finished _) = true; fun task_parents deps (parents: string list) = map (the o AList.lookup (op =) deps) parents; val schedule_seq = String_Graph.schedule (fn deps => fn (_, task) => (case task of Task (parents, body) => let val result = body (task_parents deps parents); val _ = Par_Exn.release_all (join_theory result); val _ = result_present result (); val _ = result_commit result (); in result_theory result end | Finished thy => thy)) #> ignore; val schedule_futures = Thread_Attributes.uninterruptible (fn _ => fn tasks => let val futures = tasks |> String_Graph.schedule (fn deps => fn (name, task) => (case task of Task (parents, body) => (singleton o Future.forks) {name = "theory:" ^ name, group = NONE, deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true} (fn () => (case filter (not o can Future.join o #2) deps of [] => body (map (result_theory o Future.join) (task_parents deps parents)) | bad => error ("Failed to load theory " ^ quote name ^ " (unresolved " ^ commas_quote (map #1 bad) ^ ")"))) | Finished theory => Future.value (theory_result theory))); val results1 = futures |> maps (fn future => (case Future.join_result future of Exn.Res result => join_theory result | Exn.Exn exn => [Exn.Exn exn])); val results2 = futures |> map_filter (Exn.get_res o Future.join_result) |> sort result_ord |> Par_List.map' {name = "present", sequential = sequential_presentation (Options.default ())} (fn result => Exn.capture (result_present result) ()); (* FIXME more precise commit order (!?) *) val results3 = futures |> map (fn future => Exn.capture (fn () => result_commit (Future.join future) ()) ()); (* FIXME avoid global Execution.reset (!??) *) val results4 = map Exn.Exn (maps Task_Queue.group_status (Execution.reset ())); val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4); in () end); (* eval theory *) fun eval_thy options master_dir header text_pos text parents = let val (name, _) = #name header; val keywords = fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents (Keyword.add_keywords (#keywords header) Keyword.empty_keywords); val spans = Outer_Syntax.parse_spans (Token.explode keywords text_pos text); val elements = Thy_Element.parse_elements keywords spans; val text_id = Position.copy_id text_pos Position.none; fun init () = Resources.begin_theory master_dir header parents; fun excursion () = let fun element_result span_elem (st, _) = let fun prepare span = let val tr = Position.setmp_thread_data text_id (fn () => Command.read_span keywords st master_dir init span) (); in Toplevel.timing (Resources.last_timing tr) tr end; val elem = Thy_Element.map_element prepare span_elem; val (results, st') = Toplevel.element_result keywords elem st; val pos' = Toplevel.pos_of (Thy_Element.last_element elem); in (results, (st', pos')) end; val (results, (end_state, end_pos)) = fold_map element_result elements (Toplevel.init_toplevel (), Position.none); val thy = Toplevel.end_theory end_pos end_state; in (results, thy) end; val (results, thy) = cond_timeit true ("theory " ^ quote name) excursion; fun present () = let val segments = (spans ~~ maps Toplevel.join_results results) |> map (fn (span, (st, tr, st')) => {span = span, prev_state = st, command = tr, state = st'}); val context: presentation_context = {options = options, file_pos = text_pos, adjust_pos = I, segments = segments}; in apply_presentation context thy end; in (thy, present, size text) end; (* require_thy -- checking database entries wrt. the file-system *) local fun required_by _ [] = "" | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")"; fun load_thy options initiators deps text (name, header_pos) keywords parents = let val {master = (thy_path, _), imports} = deps; val dir = Path.dir thy_path; val exec_id = Document_ID.make (); val id = Document_ID.print exec_id; val put_id = Position.put_id id; val _ = Execution.running Document_ID.none exec_id [] orelse raise Fail ("Failed to register execution: " ^ id); val text_pos = put_id (Path.position thy_path); val text_props = Position.properties_of text_pos; val _ = remove_thy name; val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators); val _ = Output.try_protocol_message (Markup.loading_theory name @ text_props) [XML.blob [text]]; val _ = Position.setmp_thread_data (Position.id_only id) (fn () => (parents, map #2 imports) |> ListPair.app (fn (thy, pos) => Context_Position.reports_global thy [(put_id pos, Theory.get_markup thy)])) (); val timing_start = Timing.start (); val header = Thy_Header.make (name, put_id header_pos) imports keywords; val (theory, present, weight) = eval_thy options dir header text_pos text (if name = Context.PureN then [Context.the_global_context ()] else parents); val timing_result = Timing.result timing_start; val timing_props = [Markup.theory_timing, (Markup.nameN, name)]; val _ = Output.try_protocol_message (timing_props @ Markup.timing_properties timing_result) [] fun commit () = update_thy deps theory; in Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight} end; fun check_thy_deps dir name = (case lookup_deps name of SOME NONE => (true, NONE, Position.none, get_imports name, []) | NONE => let val {master, text, theory_pos, imports, keywords} = Resources.check_thy dir name in (false, SOME (make_deps master imports, text), theory_pos, imports, keywords) end | SOME (SOME {master, ...}) => let val {master = master', text = text', theory_pos = theory_pos', imports = imports', keywords = keywords'} = Resources.check_thy dir name; val deps' = SOME (make_deps master' imports', text'); val current = #2 master = #2 master' andalso (case lookup_theory name of NONE => false | SOME theory => Resources.loaded_files_current theory); in (current, deps', theory_pos', imports', keywords') end); in fun require_thys options initiators qualifier dir strs tasks = fold_map (require_thy options initiators qualifier dir) strs tasks |>> forall I and require_thy options initiators qualifier dir (s, require_pos) tasks = let val {master_dir, theory_name, ...} = Resources.import_name qualifier dir s; in (case try (String_Graph.get_node tasks) theory_name of SOME task => (task_finished task, tasks) | NONE => let val _ = member (op =) initiators theory_name andalso error (cycle_msg initiators); val (current, deps, theory_pos, imports, keywords) = check_thy_deps master_dir theory_name handle ERROR msg => cat_error msg ("The error(s) above occurred for theory " ^ quote theory_name ^ Position.here require_pos ^ required_by "\n" initiators); val qualifier' = Resources.theory_qualifier theory_name; val dir' = dir + master_dir_deps (Option.map #1 deps); val parents = map (#theory_name o Resources.import_name qualifier' dir' o #1) imports; val (parents_current, tasks') = require_thys options (theory_name :: initiators) qualifier' dir' imports tasks; val all_current = current andalso parents_current; val task = if all_current then Finished (get_theory theory_name) else (case deps of NONE => raise Fail "Malformed deps" | SOME (dep, text) => Task (parents, load_thy options initiators dep text (theory_name, theory_pos) keywords)); val tasks'' = new_entry theory_name parents task tasks'; in (all_current, tasks'') end) end; end; (* use theories *) fun use_theories options qualifier imports = let val (_, tasks) = require_thys options [] qualifier Path.current imports String_Graph.empty in if Multithreading.max_threads () > 1 then schedule_futures tasks else schedule_seq tasks end; fun use_thy name = use_theories (Options.default ()) Resources.default_qualifier [(name, Position.none)]; (* toplevel scripting -- without maintaining database *) fun script_thy pos txt thy = let val trs = Outer_Syntax.parse_text thy (K thy) pos txt; val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs); val end_state = fold (Toplevel.command_exception true) trs (Toplevel.init_toplevel ()); in Toplevel.end_theory end_pos end_state end; (* register theory *) fun register_thy theory = let val name = Context.theory_long_name theory; val {master, ...} = Resources.check_thy (Resources.master_directory theory) name; val imports = Resources.imports_of theory; in change_thys (fn thys => let val thys' = remove name thys; val _ = writeln ("Registering theory " ^ quote name); in update (make_deps master imports) theory thys' end) end; (* finish all theories *) fun finish () = change_thys (String_Graph.map (fn _ => fn (_, entry) => (NONE, entry))); end; fun use_thy name = Runtime.toplevel_program (fn () => Thy_Info.use_thy name); diff --git a/src/Pure/Tools/doc.ML b/src/Pure/Tools/doc.ML --- a/src/Pure/Tools/doc.ML +++ b/src/Pure/Tools/doc.ML @@ -1,24 +1,24 @@ (* Title: Pure/Tools/doc.ML Author: Makarius Access to Isabelle documentation. *) signature DOC = sig val check: Proof.context -> string * Position.T -> string end; structure Doc: DOC = struct fun check ctxt arg = Completion.check_item "documentation" (Markup.doc o #1) (\<^scala>\doc_names\ "" |> split_lines |> map (rpair ())) ctxt arg; val _ = Theory.setup - (Thy_Output.antiquotation_verbatim_embedded \<^binding>\doc\ + (Document_Output.antiquotation_verbatim_embedded \<^binding>\doc\ (Scan.lift Parse.embedded_position) check); end; diff --git a/src/Pure/Tools/jedit.ML b/src/Pure/Tools/jedit.ML --- a/src/Pure/Tools/jedit.ML +++ b/src/Pure/Tools/jedit.ML @@ -1,90 +1,90 @@ (* Title: Pure/Tools/jedit.ML Author: Makarius Support for Isabelle/jEdit. *) signature JEDIT = sig val get_actions: unit -> string list val check_action: string * Position.T -> string end; structure JEdit: JEDIT = struct (* parse XML *) fun parse_named a (XML.Elem ((b, props), _)) = (case Properties.get props "NAME" of SOME name => if a = b then [name] else [] | NONE => []) | parse_named _ _ = []; fun parse_actions (XML.Elem (("ACTIONS", _), body)) = maps (parse_named "ACTION") body | parse_actions _ = []; fun parse_dockables (XML.Elem (("DOCKABLES", _), body)) = maps (parse_named "DOCKABLE") body |> maps (fn a => [a, a ^ "-toggle", a ^ "-float"]) | parse_dockables _ = []; (* XML resources *) val xml_file = XML.parse o File.read; fun xml_resource name = let val res = Isabelle_System.bash_process ("unzip -p \"$JEDIT_HOME/dist/jedit.jar\" " ^ Bash.string name); val rc = Process_Result.rc res; in res |> Process_Result.check |> Process_Result.out |> XML.parse handle ERROR _ => error ("Cannot unzip jedit.jar\nreturn code = " ^ string_of_int rc) end; (* actions *) val lazy_actions = Lazy.lazy (fn () => (parse_actions (xml_file \<^file>\~~/src/Tools/jEdit/src/actions.xml\) @ parse_dockables (xml_file \<^file>\~~/src/Tools/jEdit/src/dockables.xml\) @ parse_actions (xml_resource "org/gjt/sp/jedit/actions.xml") @ parse_dockables (xml_resource "org/gjt/sp/jedit/dockables.xml")) |> sort_strings); fun get_actions () = Lazy.force lazy_actions; fun check_action (name, pos) = if member (op =) (get_actions ()) name then let val ((bg1, bg2), en) = YXML.output_markup_elem (Active.make_markup Markup.jedit_actionN {implicit = false, properties = []}); val msg = "Invoke " ^ bg1 ^ name ^ bg2 ^ name ^ en ^ " jEdit action"; in writeln (msg ^ Position.here pos); name end else let val completion_report = Completion.make_report (name, pos) (fn completed => get_actions () |> filter completed |> sort_strings |> map (fn a => (a, ("action", a)))); in error ("Bad jEdit action " ^ quote name ^ Position.here pos ^ completion_report) end; val _ = Theory.setup - (Thy_Output.antiquotation_verbatim_embedded \<^binding>\action\ (Scan.lift Args.embedded_position) + (Document_Output.antiquotation_verbatim_embedded \<^binding>\action\ (Scan.lift Args.embedded_position) (fn ctxt => fn (name, pos) => let val _ = if Context_Position.is_reported ctxt pos then ignore (check_action (name, pos)) else (); in name end)); end; diff --git a/src/Pure/Tools/rail.ML b/src/Pure/Tools/rail.ML --- a/src/Pure/Tools/rail.ML +++ b/src/Pure/Tools/rail.ML @@ -1,392 +1,392 @@ (* Title: Pure/Tools/rail.ML Author: Michael Kerscher, TU München Author: Makarius Railroad diagrams in LaTeX. *) signature RAIL = sig datatype rails = Cat of int * rail list and rail = Bar of rails list | Plus of rails * rails | Newline of int | Nonterminal of string | Terminal of bool * string | Antiquote of bool * Antiquote.antiq val read: Proof.context -> Input.source -> (string Antiquote.antiquote * rail) list val output_rules: Proof.context -> (string Antiquote.antiquote * rail) list -> Latex.text end; structure Rail: RAIL = struct (** lexical syntax **) (* singleton keywords *) val keywords = Symtab.make [ ("|", Markup.keyword3), ("*", Markup.keyword3), ("+", Markup.keyword3), ("?", Markup.keyword3), ("(", Markup.empty), (")", Markup.empty), ("\", Markup.keyword2), (";", Markup.keyword2), (":", Markup.keyword2), ("@", Markup.keyword1)]; (* datatype token *) datatype kind = Keyword | Ident | String | Space | Comment of Comment.kind | Antiq of Antiquote.antiq | EOF; datatype token = Token of Position.range * (kind * string); fun pos_of (Token ((pos, _), _)) = pos; fun end_pos_of (Token ((_, pos), _)) = pos; fun range_of (toks as tok :: _) = let val pos' = end_pos_of (List.last toks) in Position.range (pos_of tok, pos') end | range_of [] = Position.no_range; fun kind_of (Token (_, (k, _))) = k; fun content_of (Token (_, (_, x))) = x; fun is_proper (Token (_, (Space, _))) = false | is_proper (Token (_, (Comment _, _))) = false | is_proper _ = true; (* diagnostics *) val print_kind = fn Keyword => "rail keyword" | Ident => "identifier" | String => "single-quoted string" | Space => "white space" | Comment _ => "formal comment" | Antiq _ => "antiquotation" | EOF => "end-of-input"; fun print (Token ((pos, _), (k, x))) = (if k = EOF then print_kind k else print_kind k ^ " " ^ quote x) ^ Position.here pos; fun print_keyword x = print_kind Keyword ^ " " ^ quote x; fun reports_of_token (Token ((pos, _), (Keyword, x))) = map (pair pos) (the_list (Symtab.lookup keywords x) @ Completion.suppress_abbrevs x) | reports_of_token (Token ((pos, _), (String, _))) = [(pos, Markup.inner_string)] | reports_of_token (Token (_, (Antiq antiq, _))) = Antiquote.antiq_reports [Antiquote.Antiq antiq] | reports_of_token _ = []; (* stopper *) fun mk_eof pos = Token ((pos, Position.none), (EOF, "")); val eof = mk_eof Position.none; fun is_eof (Token (_, (EOF, _))) = true | is_eof _ = false; val stopper = Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof; (* tokenize *) local fun token k ss = [Token (Symbol_Pos.range ss, (k, Symbol_Pos.content ss))]; fun antiq_token antiq = [Token (#range antiq, (Antiq antiq, Symbol_Pos.content (#body antiq)))]; val scan_space = Scan.many1 (Symbol.is_blank o Symbol_Pos.symbol); val scan_keyword = Scan.one (Symtab.defined keywords o Symbol_Pos.symbol); val err_prefix = "Rail lexical error: "; val scan_token = scan_space >> token Space || Comment.scan_inner >> (fn (kind, ss) => token (Comment kind) ss) || Antiquote.scan_antiq >> antiq_token || scan_keyword >> (token Keyword o single) || Lexicon.scan_id >> token Ident || Symbol_Pos.scan_string_q err_prefix >> (fn (pos1, (ss, pos2)) => [Token (Position.range (pos1, pos2), (String, Symbol_Pos.content ss))]); val scan = Scan.repeats scan_token --| Symbol_Pos.!!! (fn () => err_prefix ^ "bad input") (Scan.ahead (Scan.one Symbol_Pos.is_eof)); in val tokenize = #1 o Scan.error (Scan.finite Symbol_Pos.stopper scan); end; (** parsing **) (* parser combinators *) fun !!! scan = let val prefix = "Rail syntax error"; fun get_pos [] = " (end-of-input)" | get_pos (tok :: _) = Position.here (pos_of tok); fun err (toks, NONE) = (fn () => prefix ^ get_pos toks) | err (toks, SOME msg) = (fn () => let val s = msg () in if String.isPrefix prefix s then s else prefix ^ get_pos toks ^ ": " ^ s end); in Scan.!! err scan end; fun $$$ x = Scan.one (fn tok => kind_of tok = Keyword andalso content_of tok = x) || Scan.fail_with (fn [] => (fn () => print_keyword x ^ " expected,\nbut end-of-input was found") | tok :: _ => (fn () => print_keyword x ^ " expected,\nbut " ^ print tok ^ " was found")); fun enum1 sep scan = scan ::: Scan.repeat ($$$ sep |-- !!! scan); fun enum sep scan = enum1 sep scan || Scan.succeed []; val ident = Scan.some (fn tok => if kind_of tok = Ident then SOME (content_of tok) else NONE); val string = Scan.some (fn tok => if kind_of tok = String then SOME (content_of tok) else NONE); val antiq = Scan.some (fn tok => (case kind_of tok of Antiq a => SOME a | _ => NONE)); fun RANGE scan = Scan.trace scan >> apsnd range_of; fun RANGE_APP scan = RANGE scan >> (fn (f, r) => f r); (* parse trees *) datatype trees = CAT of tree list * Position.range and tree = BAR of trees list * Position.range | STAR of (trees * trees) * Position.range | PLUS of (trees * trees) * Position.range | MAYBE of tree * Position.range | NEWLINE of Position.range | NONTERMINAL of string * Position.range | TERMINAL of (bool * string) * Position.range | ANTIQUOTE of (bool * Antiquote.antiq) * Position.range; fun reports_of_tree ctxt = if Context_Position.reports_enabled ctxt then let fun reports r = if r = Position.no_range then [] else [(Position.range_position r, Markup.expression "")]; fun trees (CAT (ts, r)) = reports r @ maps tree ts and tree (BAR (Ts, r)) = reports r @ maps trees Ts | tree (STAR ((T1, T2), r)) = reports r @ trees T1 @ trees T2 | tree (PLUS ((T1, T2), r)) = reports r @ trees T1 @ trees T2 | tree (MAYBE (t, r)) = reports r @ tree t | tree (NEWLINE r) = reports r | tree (NONTERMINAL (_, r)) = reports r | tree (TERMINAL (_, r)) = reports r | tree (ANTIQUOTE (_, r)) = reports r; in distinct (op =) o tree end else K []; local val at_mode = Scan.option ($$$ "@") >> (fn NONE => false | _ => true); fun body x = (RANGE (enum1 "|" body1) >> BAR) x and body0 x = (RANGE (enum "|" body1) >> BAR) x and body1 x = (RANGE_APP (body2 :|-- (fn a => $$$ "*" |-- !!! body4e >> (fn b => fn r => CAT ([STAR ((a, b), r)], r)) || $$$ "+" |-- !!! body4e >> (fn b => fn r => CAT ([PLUS ((a, b), r)], r)) || Scan.succeed (K a)))) x and body2 x = (RANGE (Scan.repeat1 body3) >> CAT) x and body3 x = (RANGE_APP (body4 :|-- (fn a => $$$ "?" >> K (curry MAYBE a) || Scan.succeed (K a)))) x and body4 x = ($$$ "(" |-- !!! (body0 --| $$$ ")") || RANGE_APP ($$$ "\" >> K NEWLINE || ident >> curry NONTERMINAL || at_mode -- string >> curry TERMINAL || at_mode -- antiq >> curry ANTIQUOTE)) x and body4e x = (RANGE (Scan.option body4) >> (fn (a, r) => CAT (the_list a, r))) x; val rule_name = ident >> Antiquote.Text || antiq >> Antiquote.Antiq; val rule = rule_name -- ($$$ ":" |-- !!! body) || body >> pair (Antiquote.Text ""); val rules = enum1 ";" (Scan.option rule) >> map_filter I; in fun parse_rules toks = #1 (Scan.error (Scan.finite stopper (rules --| !!! (Scan.ahead (Scan.one is_eof)))) toks); end; (** rail expressions **) (* datatype *) datatype rails = Cat of int * rail list and rail = Bar of rails list | Plus of rails * rails | Newline of int | Nonterminal of string | Terminal of bool * string | Antiquote of bool * Antiquote.antiq; fun is_newline (Newline _) = true | is_newline _ = false; (* prepare *) local fun cat rails = Cat (0, rails); val empty = cat []; fun is_empty (Cat (_, [])) = true | is_empty _ = false; fun bar [Cat (_, [rail])] = rail | bar cats = Bar cats; fun reverse_cat (Cat (y, rails)) = Cat (y, rev (map reverse rails)) and reverse (Bar cats) = Bar (map reverse_cat cats) | reverse (Plus (cat1, cat2)) = Plus (reverse_cat cat1, reverse_cat cat2) | reverse x = x; fun plus (cat1, cat2) = Plus (cat1, reverse_cat cat2); in fun prepare_trees (CAT (ts, _)) = Cat (0, map prepare_tree ts) and prepare_tree (BAR (Ts, _)) = bar (map prepare_trees Ts) | prepare_tree (STAR (Ts, _)) = let val (cat1, cat2) = apply2 prepare_trees Ts in if is_empty cat2 then plus (empty, cat1) else bar [empty, cat [plus (cat1, cat2)]] end | prepare_tree (PLUS (Ts, _)) = plus (apply2 prepare_trees Ts) | prepare_tree (MAYBE (t, _)) = bar [empty, cat [prepare_tree t]] | prepare_tree (NEWLINE _) = Newline 0 | prepare_tree (NONTERMINAL (a, _)) = Nonterminal a | prepare_tree (TERMINAL (a, _)) = Terminal a | prepare_tree (ANTIQUOTE (a, _)) = Antiquote a; end; (* read *) fun read ctxt source = let val _ = Context_Position.report ctxt (Input.pos_of source) Markup.language_rail; val toks = tokenize (Input.source_explode source); val _ = Context_Position.reports ctxt (maps reports_of_token toks); val rules = parse_rules (filter is_proper toks); val _ = Context_Position.reports ctxt (maps (reports_of_tree ctxt o #2) rules); in map (apsnd prepare_tree) rules end; (* latex output *) local fun vertical_range_cat (Cat (_, rails)) y = let val (rails', (_, y')) = fold_map (fn rail => fn (y0, y') => if is_newline rail then (Newline (y' + 1), (y' + 1, y' + 2)) else let val (rail', y0') = vertical_range rail y0; in (rail', (y0, Int.max (y0', y'))) end) rails (y, y + 1) in (Cat (y, rails'), y') end and vertical_range (Bar cats) y = let val (cats', y') = fold_map vertical_range_cat cats y in (Bar cats', Int.max (y + 1, y')) end | vertical_range (Plus (cat1, cat2)) y = let val ([cat1', cat2'], y') = fold_map vertical_range_cat [cat1, cat2] y; in (Plus (cat1', cat2'), Int.max (y + 1, y')) end | vertical_range (Newline _) y = (Newline (y + 2), y + 3) | vertical_range atom y = (atom, y + 1); in fun output_rules ctxt rules = let val output_antiq = Antiquote.Antiq #> Document_Antiquotation.evaluate (single o Latex.symbols) ctxt #> Latex.output_text; fun output_text b s = Output.output s |> b ? enclose "\\isakeyword{" "}" |> enclose "\\isa{" "}"; fun output_cat c (Cat (_, rails)) = outputs c rails and outputs c [rail] = output c rail | outputs _ rails = implode (map (output "") rails) and output _ (Bar []) = "" | output c (Bar [cat]) = output_cat c cat | output _ (Bar (cat :: cats)) = "\\rail@bar\n" ^ output_cat "" cat ^ implode (map (fn Cat (y, rails) => "\\rail@nextbar{" ^ string_of_int y ^ "}\n" ^ outputs "" rails) cats) ^ "\\rail@endbar\n" | output c (Plus (cat, Cat (y, rails))) = "\\rail@plus\n" ^ output_cat c cat ^ "\\rail@nextplus{" ^ string_of_int y ^ "}\n" ^ outputs "c" rails ^ "\\rail@endplus\n" | output _ (Newline y) = "\\rail@cr{" ^ string_of_int y ^ "}\n" | output c (Nonterminal s) = "\\rail@" ^ c ^ "nont{" ^ output_text false s ^ "}[]\n" | output c (Terminal (b, s)) = "\\rail@" ^ c ^ "term{" ^ output_text b s ^ "}[]\n" | output c (Antiquote (b, a)) = "\\rail@" ^ c ^ (if b then "term{" else "nont{") ^ output_antiq a ^ "}[]\n"; fun output_rule (name, rail) = let val (rail', y') = vertical_range rail 0; val out_name = (case name of Antiquote.Text "" => "" | Antiquote.Text s => output_text false s | Antiquote.Antiq a => output_antiq a); in "\\rail@begin{" ^ string_of_int y' ^ "}{" ^ out_name ^ "}\n" ^ output "" rail' ^ "\\rail@end\n" end; in Latex.string (Latex.environment "railoutput" (implode (map output_rule rules))) end; val _ = Theory.setup - (Thy_Output.antiquotation_raw_embedded \<^binding>\rail\ (Scan.lift Args.text_input) + (Document_Output.antiquotation_raw_embedded \<^binding>\rail\ (Scan.lift Args.text_input) (fn ctxt => output_rules ctxt o read ctxt)); end; end; diff --git a/src/Pure/pure_syn.ML b/src/Pure/pure_syn.ML --- a/src/Pure/pure_syn.ML +++ b/src/Pure/pure_syn.ML @@ -1,81 +1,81 @@ (* Title: Pure/pure_syn.ML Author: Makarius Outer syntax for bootstrapping: commands that are accessible outside a regular theory context. *) signature PURE_SYN = sig val document_command: {markdown: bool} -> (xstring * Position.T) option * Input.source -> Toplevel.transition -> Toplevel.transition val bootstrap_thy: theory end; structure Pure_Syn: PURE_SYN = struct val semi = Scan.option (Parse.$$$ ";"); fun output_document state markdown txt = let val ctxt = Toplevel.presentation_context state; - val _ = Context_Position.reports ctxt (Thy_Output.document_reports txt); - in Thy_Output.output_document ctxt markdown txt end; + val _ = Context_Position.reports ctxt (Document_Output.document_reports txt); + in Document_Output.output_document ctxt markdown txt end; fun document_command markdown (loc, txt) = Toplevel.keep (fn state => (case loc of NONE => ignore (output_document state markdown txt) | SOME (_, pos) => error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o Toplevel.present_local_theory loc (fn state => ignore (output_document state markdown txt)); val _ = Outer_Syntax.command ("chapter", \<^here>) "chapter heading" (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false}); val _ = Outer_Syntax.command ("section", \<^here>) "section heading" (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false}); val _ = Outer_Syntax.command ("subsection", \<^here>) "subsection heading" (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false}); val _ = Outer_Syntax.command ("subsubsection", \<^here>) "subsubsection heading" (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false}); val _ = Outer_Syntax.command ("paragraph", \<^here>) "paragraph heading" (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false}); val _ = Outer_Syntax.command ("subparagraph", \<^here>) "subparagraph heading" (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false}); val _ = Outer_Syntax.command ("text", \<^here>) "formal comment (primary style)" (Parse.opt_target -- Parse.document_source >> document_command {markdown = true}); val _ = Outer_Syntax.command ("txt", \<^here>) "formal comment (secondary style)" (Parse.opt_target -- Parse.document_source >> document_command {markdown = true}); val _ = Outer_Syntax.command ("text_raw", \<^here>) "LaTeX text (without surrounding environment)" (Parse.opt_target -- Parse.document_source >> document_command {markdown = true}); val _ = Outer_Syntax.command ("theory", \<^here>) "begin theory" (Thy_Header.args >> (fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization"))); val bootstrap_thy = Context.the_global_context (); val _ = Theory.setup (Config.put_global Outer_Syntax.bootstrap false); end; diff --git a/src/Tools/Code/code_target.ML b/src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML +++ b/src/Tools/Code/code_target.ML @@ -1,797 +1,797 @@ (* Title: Tools/Code/code_target.ML Author: Florian Haftmann, TU Muenchen Generic infrastructure for target language data. *) signature CODE_TARGET = sig val cert_tyco: Proof.context -> string -> string val read_tyco: Proof.context -> string -> string datatype pretty_modules = Singleton of string * Pretty.T | Hierarchy of (string list * Pretty.T) list; val next_export: theory -> string * theory val export_code_for: ({physical: bool} * (Path.T * Position.T)) option -> string -> string -> int option -> Token.T list -> Code_Thingol.program -> bool -> Code_Symbol.T list -> local_theory -> local_theory val produce_code_for: Proof.context -> string -> string -> int option -> Token.T list -> Code_Thingol.program -> bool -> Code_Symbol.T list -> (string list * string) list * string option list val present_code_for: Proof.context -> string -> string -> int option -> Token.T list -> Code_Thingol.program -> Code_Symbol.T list * Code_Symbol.T list -> string val check_code_for: string -> bool -> Token.T list -> Code_Thingol.program -> bool -> Code_Symbol.T list -> local_theory -> local_theory val export_code: bool -> string list -> (((string * string) * ({physical: bool} * (Path.T * Position.T)) option) * Token.T list) list -> local_theory -> local_theory val export_code_cmd: bool -> string list -> (((string * string) * ({physical: bool} * Input.source) option) * Token.T list) list -> local_theory -> local_theory val produce_code: Proof.context -> bool -> string list -> string -> string -> int option -> Token.T list -> (string list * string) list * string option list val present_code: Proof.context -> string list -> Code_Symbol.T list -> string -> string -> int option -> Token.T list -> string val check_code: bool -> string list -> ((string * bool) * Token.T list) list -> local_theory -> local_theory val codeN: string val generatedN: string val code_path: Path.T -> Path.T val code_export_message: theory -> unit val export: Path.binding -> string -> theory -> theory val compilation_text: Proof.context -> string -> Code_Thingol.program -> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm -> (string list * string) list * string val compilation_text': Proof.context -> string -> string option -> Code_Thingol.program -> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm -> ((string list * string) list * string) * (Code_Symbol.T -> string option) type serializer type literals = Code_Printer.literals type language type ancestry val assert_target: theory -> string -> string val add_language: string * language -> theory -> theory val add_derived_target: string * ancestry -> theory -> theory val the_literals: Proof.context -> string -> literals val parse_args: 'a parser -> Token.T list -> 'a val default_code_width: int Config.T type ('a, 'b, 'c, 'd, 'e, 'f) symbol_attr_decl val set_identifiers: (string, string, string, string, string, string) symbol_attr_decl -> theory -> theory val set_printings: (Code_Printer.raw_const_syntax, Code_Printer.tyco_syntax, string, unit, unit, string * Code_Symbol.T list) symbol_attr_decl -> theory -> theory val add_reserved: string -> string -> theory -> theory end; structure Code_Target : CODE_TARGET = struct open Basic_Code_Symbol; open Basic_Code_Thingol; type literals = Code_Printer.literals; type ('a, 'b, 'c, 'd, 'e, 'f) symbol_attr_decl = (string * (string * 'a option) list, string * (string * 'b option) list, class * (string * 'c option) list, (class * class) * (string * 'd option) list, (class * string) * (string * 'e option) list, string * (string * 'f option) list) Code_Symbol.attr; type tyco_syntax = Code_Printer.tyco_syntax; type raw_const_syntax = Code_Printer.raw_const_syntax; (** checking and parsing of symbols **) fun cert_const ctxt const = let val _ = if Sign.declared_const (Proof_Context.theory_of ctxt) const then () else error ("No such constant: " ^ quote const); in const end; fun read_const ctxt = Code.read_const (Proof_Context.theory_of ctxt); fun cert_tyco ctxt tyco = let val _ = if Sign.declared_tyname (Proof_Context.theory_of ctxt) tyco then () else error ("No such type constructor: " ^ quote tyco); in tyco end; fun read_tyco ctxt = #1 o dest_Type o Proof_Context.read_type_name {proper = true, strict = true} ctxt; fun cert_class ctxt class = let val _ = Axclass.get_info (Proof_Context.theory_of ctxt) class; in class end; val parse_classrel_ident = Parse.class --| \<^keyword>\<\ -- Parse.class; fun cert_inst ctxt (class, tyco) = (cert_class ctxt class, cert_tyco ctxt tyco); fun read_inst ctxt (raw_tyco, raw_class) = (read_tyco ctxt raw_tyco, Proof_Context.read_class ctxt raw_class); val parse_inst_ident = Parse.name --| \<^keyword>\::\ -- Parse.class; fun cert_syms ctxt = Code_Symbol.map_attr (cert_const ctxt) (cert_tyco ctxt) (cert_class ctxt) (apply2 (cert_class ctxt)) (cert_inst ctxt) I; fun read_syms ctxt = Code_Symbol.map_attr (read_const ctxt) (read_tyco ctxt) (Proof_Context.read_class ctxt) (apply2 (Proof_Context.read_class ctxt)) (read_inst ctxt) I; fun cert_syms' ctxt = Code_Symbol.map_attr (apfst (cert_const ctxt)) (apfst (cert_tyco ctxt)) (apfst (cert_class ctxt)) ((apfst o apply2) (cert_class ctxt)) (apfst (cert_inst ctxt)) I; fun read_syms' ctxt = Code_Symbol.map_attr (apfst (read_const ctxt)) (apfst (read_tyco ctxt)) (apfst (Proof_Context.read_class ctxt)) ((apfst o apply2) (Proof_Context.read_class ctxt)) (apfst (read_inst ctxt)) I; fun check_name is_module s = let val _ = if s = "" then error "Bad empty code name" else (); val xs = Long_Name.explode s; val xs' = if is_module then map (Name.desymbolize NONE) xs else if length xs < 2 then error ("Bad code name without module component: " ^ quote s) else let val (ys, y) = split_last xs; val ys' = map (Name.desymbolize NONE) ys; val y' = Name.desymbolize NONE y; in ys' @ [y'] end; in if xs' = xs then if is_module then (xs, "") else split_last xs else error ("Invalid code name: " ^ quote s ^ "\n" ^ "better try " ^ quote (Long_Name.implode xs')) end; (** theory data **) datatype pretty_modules = Singleton of string * Pretty.T | Hierarchy of (string list * Pretty.T) list; type serializer = Token.T list -> Proof.context -> { reserved_syms: string list, identifiers: Code_Printer.identifiers, includes: (string * Pretty.T) list, class_syntax: string -> string option, tyco_syntax: string -> Code_Printer.tyco_syntax option, const_syntax: string -> Code_Printer.const_syntax option, module_name: string } -> Code_Thingol.program -> Code_Symbol.T list -> pretty_modules * (Code_Symbol.T -> string option); type language = {serializer: serializer, literals: literals, check: {env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string}, evaluation_args: Token.T list}; type ancestry = (string * (Code_Thingol.program -> Code_Thingol.program)) list; val merge_ancestry : ancestry * ancestry -> ancestry = AList.join (op =) (K snd); type target = {serial: serial, language: language, ancestry: ancestry}; structure Targets = Theory_Data ( type T = (target * Code_Printer.data) Symtab.table * int; val empty = (Symtab.empty, 0); val extend = I; fun merge ((targets1, index1), (targets2, index2)) : T = let val targets' = Symtab.join (fn target_name => fn ((target1, data1), (target2, data2)) => if #serial target1 = #serial target2 then ({serial = #serial target1, language = #language target1, ancestry = merge_ancestry (#ancestry target1, #ancestry target2)}, Code_Printer.merge_data (data1, data2)) else error ("Incompatible targets: " ^ quote target_name)) (targets1, targets2) val index' = Int.max (index1, index2); in (targets', index') end; ); val exists_target = Symtab.defined o #1 o Targets.get; val lookup_target_data = Symtab.lookup o #1 o Targets.get; fun assert_target thy target_name = if exists_target thy target_name then target_name else error ("Unknown code target language: " ^ quote target_name); fun reset_index thy = if #2 (Targets.get thy) = 0 then NONE else SOME ((Targets.map o apsnd) (K 0) thy); val _ = Theory.setup (Theory.at_begin reset_index); fun next_export thy = let val thy' = (Targets.map o apsnd) (fn i => i + 1) thy; val i = #2 (Targets.get thy'); in ("export" ^ string_of_int i, thy') end; fun fold1 f xs = fold f (tl xs) (hd xs); fun join_ancestry thy target_name = let val _ = assert_target thy target_name; val the_target_data = the o lookup_target_data thy; val (target, this_data) = the_target_data target_name; val ancestry = #ancestry target; val modifies = rev (map snd ancestry); val modify = fold (curry (op o)) modifies I; val datas = rev (map (snd o the_target_data o fst) ancestry) @ [this_data]; val data = fold1 (fn data' => fn data => Code_Printer.merge_data (data, data')) datas; in (modify, (target, data)) end; fun allocate_target target_name target thy = let val _ = if exists_target thy target_name then error ("Attempt to overwrite existing target " ^ quote target_name) else (); in thy |> (Targets.map o apfst o Symtab.update) (target_name, (target, Code_Printer.empty_data)) end; fun add_language (target_name, language) = allocate_target target_name {serial = serial (), language = language, ancestry = []}; fun add_derived_target (target_name, initial_ancestry) thy = let val _ = if null initial_ancestry then error "Must derive from existing target(s)" else (); fun the_target_data target_name' = case lookup_target_data thy target_name' of NONE => error ("Unknown code target language: " ^ quote target_name') | SOME target_data' => target_data'; val targets = rev (map (fst o the_target_data o fst) initial_ancestry); val supremum = fold1 (fn target' => fn target => if #serial target = #serial target' then target else error "Incompatible targets") targets; val ancestries = map #ancestry targets @ [initial_ancestry]; val ancestry = fold1 (fn ancestry' => fn ancestry => merge_ancestry (ancestry, ancestry')) ancestries; in allocate_target target_name {serial = #serial supremum, language = #language supremum, ancestry = ancestry} thy end; fun map_data target_name f thy = let val _ = assert_target thy target_name; in thy |> (Targets.map o apfst o Symtab.map_entry target_name o apsnd o Code_Printer.map_data) f end; fun map_reserved target_name = map_data target_name o @{apply 3(1)}; fun map_identifiers target_name = map_data target_name o @{apply 3(2)}; fun map_printings target_name = map_data target_name o @{apply 3(3)}; (** serializers **) val codeN = "code"; val generatedN = "Generated_Code"; val code_path = Path.append (Path.basic codeN); fun code_export_message thy = writeln (Export.message thy (Path.basic codeN)); fun export binding content thy = let val thy' = thy |> Generated_Files.add_files (binding, content); val _ = Export.export thy' binding [XML.Text content]; in thy' end; local fun export_logical (file_prefix, file_pos) format pretty_modules = let fun binding path = Path.binding (path, file_pos); val prefix = code_path file_prefix; in (case pretty_modules of Singleton (ext, p) => export (binding (Path.ext ext prefix)) (format p) | Hierarchy modules => fold (fn (names, p) => export (binding (prefix + Path.make names)) (format p)) modules) #> tap code_export_message end; fun export_physical root format pretty_modules = (case pretty_modules of Singleton (_, p) => File.write root (format p) | Hierarchy code_modules => (Isabelle_System.make_directory root; List.app (fn (names, p) => File.write (Path.appends (root :: map Path.basic names)) (format p)) code_modules)); in fun export_result some_file format (pretty_code, _) thy = (case some_file of NONE => let val (file_prefix, thy') = next_export thy; in export_logical (Path.basic file_prefix, Position.none) format pretty_code thy' end | SOME ({physical = false}, file_prefix) => export_logical file_prefix format pretty_code thy | SOME ({physical = true}, (file, _)) => let val root = File.full_path (Resources.master_directory thy) file; val _ = File.check_dir (Path.dir root); val _ = export_physical root format pretty_code; in thy end); fun produce_result syms width pretty_modules = let val format = Code_Printer.format [] width in (case pretty_modules of (Singleton (_, p), deresolve) => ([([], format p)], map deresolve syms) | (Hierarchy code_modules, deresolve) => ((map o apsnd) format code_modules, map deresolve syms)) end; fun present_result selects width (pretty_modules, _) = let val format = Code_Printer.format selects width in (case pretty_modules of Singleton (_, p) => format p | Hierarchy code_modules => space_implode "\n\n" (map (format o #2) code_modules)) end; end; (** serializer usage **) (* technical aside: pretty printing width *) val default_code_width = Attrib.setup_config_int \<^binding>\default_code_width\ (K 80); fun default_width ctxt = Config.get ctxt default_code_width; val the_width = the_default o default_width; (* montage *) fun the_language ctxt = #language o fst o the o lookup_target_data (Proof_Context.theory_of ctxt); fun the_literals ctxt = #literals o the_language ctxt; fun the_evaluation_args ctxt = #evaluation_args o the_language ctxt; local fun activate_target ctxt target_name = let val thy = Proof_Context.theory_of ctxt; val (modify, (target, data)) = join_ancestry thy target_name; val serializer = (#serializer o #language) target; in { serializer = serializer, data = data, modify = modify } end; fun project_program_for_syms ctxt syms_hidden syms1 program1 = let val syms2 = subtract (op =) syms_hidden syms1; val program2 = Code_Symbol.Graph.restrict (not o member (op =) syms_hidden) program1; val unimplemented = Code_Thingol.unimplemented program2; val _ = if null unimplemented then () else error ("No code equations for " ^ commas (map (Proof_Context.markup_const ctxt) unimplemented)); val syms3 = Code_Symbol.Graph.all_succs program2 syms2; val program3 = Code_Symbol.Graph.restrict (member (op =) syms3) program2; in program3 end; fun project_includes_for_syms syms includes = let fun select_include (name, (content, cs)) = if null cs orelse exists (member (op =) syms) cs then SOME (name, content) else NONE; in map_filter select_include includes end; fun prepare_serializer ctxt target_name module_name args proto_program syms = let val { serializer, data, modify } = activate_target ctxt target_name; val printings = Code_Printer.the_printings data; val _ = if module_name = "" then () else (check_name true module_name; ()) val hidden_syms = Code_Symbol.symbols_of printings; val prepared_program = project_program_for_syms ctxt hidden_syms syms proto_program; val prepared_syms = subtract (op =) hidden_syms syms; val all_syms = Code_Symbol.Graph.all_succs proto_program syms; val includes = project_includes_for_syms all_syms (Code_Symbol.dest_module_data printings); val prepared_serializer = serializer args ctxt { reserved_syms = Code_Printer.the_reserved data, identifiers = Code_Printer.the_identifiers data, includes = includes, const_syntax = Code_Symbol.lookup_constant_data printings, tyco_syntax = Code_Symbol.lookup_type_constructor_data printings, class_syntax = Code_Symbol.lookup_type_class_data printings, module_name = module_name }; in (prepared_serializer o modify, (prepared_program, prepared_syms)) end; fun invoke_serializer ctxt target_name module_name args program all_public syms = let val (prepared_serializer, (prepared_program, prepared_syms)) = prepare_serializer ctxt target_name module_name args program syms; val exports = if all_public then [] else prepared_syms; in Code_Preproc.timed_exec "serializing" (fn () => prepared_serializer prepared_program exports) ctxt end; fun assert_module_name "" = error "Empty module name not allowed here" | assert_module_name module_name = module_name; in fun export_code_for some_file target_name module_name some_width args program all_public cs lthy = let val format = Code_Printer.format [] (the_width lthy some_width); val res = invoke_serializer lthy target_name module_name args program all_public cs; in Local_Theory.background_theory (export_result some_file format res) lthy end; fun produce_code_for ctxt target_name module_name some_width args = let val serializer = invoke_serializer ctxt target_name (assert_module_name module_name) args; in fn program => fn all_public => fn syms => produce_result syms (the_width ctxt some_width) (serializer program all_public syms) end; fun present_code_for ctxt target_name module_name some_width args = let val serializer = invoke_serializer ctxt target_name (assert_module_name module_name) args; in fn program => fn (syms, selects) => present_result selects (the_width ctxt some_width) (serializer program false syms) end; fun check_code_for target_name strict args program all_public syms lthy = let val { env_var, make_destination, make_command } = #check (the_language lthy target_name); val format = Code_Printer.format [] 80; fun ext_check p = let val destination = make_destination p; val lthy' = lthy |> Local_Theory.background_theory (export_result (SOME ({physical = true}, (destination, Position.none))) format (invoke_serializer lthy target_name generatedN args program all_public syms)); val cmd = make_command generatedN; val context_cmd = "cd " ^ File.bash_path p ^ " && " ^ cmd ^ " 2>&1"; in if Isabelle_System.bash context_cmd <> 0 then error ("Code check failed for " ^ target_name ^ ": " ^ cmd) else lthy' end; in if not (env_var = "") andalso getenv env_var = "" then if strict then error (env_var ^ " not set; cannot check code for " ^ target_name) else (warning (env_var ^ " not set; skipped checking code for " ^ target_name); lthy) else Isabelle_System.with_tmp_dir "Code_Test" ext_check end; fun dynamic_compilation_text prepared_serializer width prepared_program syms all_public ((vs, ty), t) = let val _ = if Code_Thingol.contains_dict_var t then error "Term to be evaluated contains free dictionaries" else (); val v' = singleton (Name.variant_list (map fst vs)) "a"; val vs' = (v', []) :: vs; val ty' = ITyVar v' `-> ty; val program = prepared_program |> Code_Symbol.Graph.new_node (Code_Symbol.value, Code_Thingol.Fun (((vs', ty'), [(([IVar (SOME "dummy")], t), (NONE, true))]), NONE)) |> fold (curry (perhaps o try o Code_Symbol.Graph.add_edge) Code_Symbol.value) syms; val (pretty_code, deresolve) = prepared_serializer program (if all_public then [] else [Code_Symbol.value]); val (compilation_code, [SOME value_name]) = produce_result [Code_Symbol.value] width (pretty_code, deresolve); in ((compilation_code, value_name), deresolve) end; fun compilation_text' ctxt target_name some_module_name program syms = let val width = default_width ctxt; val evaluation_args = the_evaluation_args ctxt target_name; val (prepared_serializer, (prepared_program, _)) = prepare_serializer ctxt target_name (the_default generatedN some_module_name) evaluation_args program syms; in Code_Preproc.timed_exec "serializing" (fn () => dynamic_compilation_text prepared_serializer width prepared_program syms) ctxt end; fun compilation_text ctxt target_name program syms = fst oo compilation_text' ctxt target_name NONE program syms end; (* local *) (* code generation *) fun prep_destination (location, source) = let val s = Input.string_of source val pos = Input.pos_of source val delimited = Input.is_delimited source in if location = {physical = false} then (location, Path.explode_pos (s, pos)) else let val _ = if s = "" then error ("Bad bad empty " ^ Markup.markup Markup.keyword2 "file" ^ " argument") else (); val _ = legacy_feature (Markup.markup Markup.keyword1 "export_code" ^ " with " ^ Markup.markup Markup.keyword2 "file" ^ " argument" ^ Position.here pos); val _ = Position.report pos (Markup.language_path delimited); val path = #1 (Path.explode_pos (s, pos)); val _ = Position.report pos (Markup.path (Path.implode_symbolic path)); in (location, (path, pos)) end end; fun export_code all_public cs seris lthy = let val program = Code_Thingol.consts_program lthy cs; in (seris, lthy) |-> fold (fn (((target_name, module_name), some_file), args) => export_code_for some_file target_name module_name NONE args program all_public (map Constant cs)) end; fun export_code_cmd all_public raw_cs seris lthy = let val cs = Code_Thingol.read_const_exprs lthy raw_cs; in export_code all_public cs ((map o apfst o apsnd o Option.map) prep_destination seris) lthy end; fun produce_code ctxt all_public cs target_name some_width some_module_name args = let val program = Code_Thingol.consts_program ctxt cs; in produce_code_for ctxt target_name some_width some_module_name args program all_public (map Constant cs) end; fun present_code ctxt cs syms target_name some_width some_module_name args = let val program = Code_Thingol.consts_program ctxt cs; in present_code_for ctxt target_name some_width some_module_name args program (map Constant cs, syms) end; fun check_code all_public cs seris lthy = let val program = Code_Thingol.consts_program lthy cs; in (seris, lthy) |-> fold (fn ((target_name, strict), args) => check_code_for target_name strict args program all_public (map Constant cs)) end; fun check_code_cmd all_public raw_cs seris lthy = check_code all_public (Code_Thingol.read_const_exprs lthy raw_cs) seris lthy; (** serializer configuration **) (* reserved symbol names *) fun add_reserved target_name sym thy = let val (_, (_, data)) = join_ancestry thy target_name; val _ = if member (op =) (Code_Printer.the_reserved data) sym then error ("Reserved symbol " ^ quote sym ^ " already declared") else (); in thy |> map_reserved target_name (insert (op =) sym) end; (* checking of syntax *) fun check_const_syntax ctxt target_name c syn = if Code_Printer.requires_args syn > Code.args_number (Proof_Context.theory_of ctxt) c then error ("Too many arguments in syntax for constant " ^ quote c) else Code_Printer.prep_const_syntax (Proof_Context.theory_of ctxt) (the_literals ctxt target_name) c syn; fun check_tyco_syntax ctxt target_name tyco syn = if fst syn <> Sign.arity_number (Proof_Context.theory_of ctxt) tyco then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco) else syn; (* custom symbol names *) fun arrange_name_decls x = let fun arrange is_module (sym, target_names) = map (fn (target, some_name) => (target, (sym, Option.map (check_name is_module) some_name))) target_names; in Code_Symbol.maps_attr' (arrange false) (arrange false) (arrange false) (arrange false) (arrange false) (arrange true) x end; fun cert_name_decls ctxt = cert_syms' ctxt #> arrange_name_decls; fun read_name_decls ctxt = read_syms' ctxt #> arrange_name_decls; fun set_identifier (target_name, sym_name) = map_identifiers target_name (Code_Symbol.set_data sym_name); fun gen_set_identifiers prep_name_decl raw_name_decls thy = fold set_identifier (prep_name_decl (Proof_Context.init_global thy) raw_name_decls) thy; val set_identifiers = gen_set_identifiers cert_name_decls; val set_identifiers_cmd = gen_set_identifiers read_name_decls; (* custom printings *) fun arrange_printings prep_syms ctxt = let fun arrange check (sym, target_syns) = map (fn (target_name, some_syn) => (target_name, (sym, Option.map (check ctxt target_name sym) some_syn))) target_syns; in Code_Symbol.maps_attr' (arrange check_const_syntax) (arrange check_tyco_syntax) (arrange ((K o K o K) I)) (arrange ((K o K o K) I)) (arrange ((K o K o K) I)) (arrange (fn ctxt => fn _ => fn _ => fn (raw_content, raw_syms) => (Pretty.blk (0, Pretty.fbreaks (map Code_Printer.str (split_lines raw_content))), map (prep_syms ctxt) raw_syms))) end; fun cert_printings ctxt = cert_syms' ctxt #> arrange_printings cert_syms ctxt; fun read_printings ctxt = read_syms' ctxt #> arrange_printings read_syms ctxt; fun set_printing (target_name, sym_syn) = map_printings target_name (Code_Symbol.set_data sym_syn); fun gen_set_printings prep_print_decl raw_print_decls thy = fold set_printing (prep_print_decl (Proof_Context.init_global thy) raw_print_decls) thy; val set_printings = gen_set_printings cert_printings; val set_printings_cmd = gen_set_printings read_printings; (* concrete syntax *) fun parse_args f args = case Scan.read Token.stopper f args of SOME x => x | NONE => error "Bad serializer arguments"; (** Isar setup **) val (constantK, type_constructorK, type_classK, class_relationK, class_instanceK, code_moduleK) = (\<^keyword>\constant\, \<^keyword>\type_constructor\, \<^keyword>\type_class\, \<^keyword>\class_relation\, \<^keyword>\class_instance\, \<^keyword>\code_module\); local val parse_constants = constantK |-- Scan.repeat1 Parse.term >> map Constant; val parse_type_constructors = type_constructorK |-- Scan.repeat1 Parse.type_const >> map Type_Constructor; val parse_classes = type_classK |-- Scan.repeat1 Parse.class >> map Type_Class; val parse_class_relations = class_relationK |-- Scan.repeat1 parse_classrel_ident >> map Class_Relation; val parse_instances = class_instanceK |-- Scan.repeat1 parse_inst_ident >> map Class_Instance; val parse_simple_symbols = Scan.repeats1 (parse_constants || parse_type_constructors || parse_classes || parse_class_relations || parse_instances); fun parse_single_symbol_pragma parse_keyword parse_isa parse_target = parse_keyword |-- Parse.!!! (parse_isa --| (\<^keyword>\\\ || \<^keyword>\=>\) -- Parse.and_list1 (\<^keyword>\(\ |-- (Parse.name --| \<^keyword>\)\ -- Scan.option parse_target))); fun parse_symbol_pragma parse_const parse_tyco parse_class parse_classrel parse_inst parse_module = parse_single_symbol_pragma constantK Parse.term parse_const >> Constant || parse_single_symbol_pragma type_constructorK Parse.type_const parse_tyco >> Type_Constructor || parse_single_symbol_pragma type_classK Parse.class parse_class >> Type_Class || parse_single_symbol_pragma class_relationK parse_classrel_ident parse_classrel >> Class_Relation || parse_single_symbol_pragma class_instanceK parse_inst_ident parse_inst >> Class_Instance || parse_single_symbol_pragma code_moduleK Parse.name parse_module >> Module; fun parse_symbol_pragmas parse_const parse_tyco parse_class parse_classrel parse_inst parse_module = Parse.enum1 "|" (Parse.group (fn () => "code symbol pragma") (parse_symbol_pragma parse_const parse_tyco parse_class parse_classrel parse_inst parse_module)); val code_expr_argsP = Scan.optional (\<^keyword>\(\ |-- Parse.args --| \<^keyword>\)\) []; fun code_expr_inP (all_public, raw_cs) = Scan.repeat (\<^keyword>\in\ |-- Parse.!!! (Parse.name -- Scan.optional (\<^keyword>\module_name\ |-- Parse.name) "" -- Scan.option ((\<^keyword>\file_prefix\ >> K {physical = false} || \<^keyword>\file\ >> K {physical = true}) -- Parse.!!! Parse.path_input) -- code_expr_argsP)) >> (fn seri_args => export_code_cmd all_public raw_cs seri_args); fun code_expr_checkingP (all_public, raw_cs) = (\<^keyword>\checking\ |-- Parse.!!! (Scan.repeat (Parse.name -- (Scan.optional (\<^keyword>\?\ >> K false) true) -- code_expr_argsP))) >> (fn seri_args => check_code_cmd all_public raw_cs seri_args); in val _ = Outer_Syntax.command \<^command_keyword>\code_reserved\ "declare words as reserved for target language" (Parse.name -- Scan.repeat1 Parse.name >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds)); val _ = Outer_Syntax.command \<^command_keyword>\code_identifier\ "declare mandatory names for code symbols" (parse_symbol_pragmas Parse.name Parse.name Parse.name Parse.name Parse.name Parse.name >> (Toplevel.theory o fold set_identifiers_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\code_printing\ "declare dedicated printing for code symbols" (parse_symbol_pragmas (Code_Printer.parse_const_syntax) (Code_Printer.parse_tyco_syntax) Parse.string (Parse.minus >> K ()) (Parse.minus >> K ()) (Parse.text -- Scan.optional (\<^keyword>\for\ |-- parse_simple_symbols) []) >> (Toplevel.theory o fold set_printings_cmd)); val _ = Outer_Syntax.local_theory \<^command_keyword>\export_code\ "generate executable code for constants" (Scan.optional (\<^keyword>\open\ >> K true) false -- Scan.repeat1 Parse.term :|-- (fn args => (code_expr_checkingP args || code_expr_inP args))); end; local val parse_const_terms = Args.theory -- Scan.repeat1 Args.term >> uncurry (fn thy => map (Code.check_const thy)); fun parse_symbols keyword parse internalize mark_symbol = Scan.lift (keyword --| Args.colon) |-- Args.theory -- Scan.repeat1 parse >> uncurry (fn thy => map (mark_symbol o internalize thy)); val parse_consts = parse_symbols constantK Args.term Code.check_const Constant; val parse_types = parse_symbols type_constructorK (Scan.lift Args.name) Sign.intern_type Type_Constructor; val parse_classes = parse_symbols type_classK (Scan.lift Args.name) Sign.intern_class Type_Class; val parse_instances = parse_symbols class_instanceK (Scan.lift (Args.name --| Args.$$$ "::" -- Args.name)) (fn thy => fn (raw_tyco, raw_class) => (Sign.intern_class thy raw_tyco, Sign.intern_type thy raw_class)) Class_Instance; in val _ = Theory.setup - (Thy_Output.antiquotation_raw \<^binding>\code_stmts\ + (Document_Output.antiquotation_raw \<^binding>\code_stmts\ (parse_const_terms -- Scan.repeats (parse_consts || parse_types || parse_classes || parse_instances) -- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int))) (fn ctxt => fn ((consts, symbols), (target_name, some_width)) => present_code ctxt consts symbols target_name "Example" some_width [] |> trim_line - |> Thy_Output.verbatim (Config.put Document_Antiquotation.thy_output_display true ctxt))); + |> Document_Output.verbatim (Config.put Document_Antiquotation.thy_output_display true ctxt))); end; end; (*struct*)