--- a/doc-src/IsarAdvanced/Codegen/IsaMakefile Fri Sep 12 12:04:20 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/IsaMakefile Sun Sep 14 21:50:35 2008 +0200
@@ -23,7 +23,7 @@
Thy: $(THY)
-$(THY): Thy/ROOT.ML Thy/Codegen.thy ../../antiquote_setup.ML
+$(THY): Thy/ROOT.ML Thy/*.thy ../../antiquote_setup.ML
@$(USEDIR) HOL Thy
--- a/doc-src/IsarAdvanced/Codegen/Makefile Fri Sep 12 12:04:20 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Makefile Sun Sep 14 21:50:35 2008 +0200
@@ -13,7 +13,7 @@
NAME = codegen
-FILES = $(NAME).tex Thy/document/Codegen.tex \
+FILES = $(NAME).tex Thy/document/*.tex \
style.sty ../../iman.sty ../../extra.sty ../../isar.sty \
../../isabelle.sty ../../isabellesym.sty ../../pdfsetup.sty \
../../manual.bib ../../proof.sty
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy Sun Sep 14 21:50:35 2008 +0200
@@ -0,0 +1,9 @@
+theory Adaption
+imports Setup
+begin
+
+section {* Adaption to target languages *}
+
+subsection {* \ldots *}
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Further.thy Sun Sep 14 21:50:35 2008 +0200
@@ -0,0 +1,17 @@
+theory Further
+imports Setup
+begin
+
+section {* Further topics *}
+
+subsection {* Serializer options *}
+
+subsection {* Evaluation oracle *}
+
+subsection {* Code antiquotation *}
+
+subsection {* Creating new targets *}
+
+text {* extending targets, adding targets *}
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy Sun Sep 14 21:50:35 2008 +0200
@@ -0,0 +1,22 @@
+theory Introduction
+imports Setup
+begin
+
+chapter {* Code generation from @{text "Isabelle/HOL"} theories *}
+
+section {* Introduction and Overview *}
+
+text {*
+ This tutorial introduces a generic code generator for the
+ Isabelle system \cite{isa-tutorial}.
+*}
+
+subsection {* Code generation via shallow embedding *}
+
+text {* example *}
+
+subsection {* Code generator architecture *}
+
+text {* foundation, forward references for yet unexplained things *}
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/ML.thy Sun Sep 14 21:50:35 2008 +0200
@@ -0,0 +1,7 @@
+theory "ML"
+imports Setup
+begin
+
+section {* ML system interfaces *}
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Program.thy Sun Sep 14 21:50:35 2008 +0200
@@ -0,0 +1,27 @@
+theory Program
+imports Setup
+begin
+
+section {* Turning Theories into Programs *}
+
+subsection {* The @{text "Isabelle/HOL"} default setup *}
+
+text {* Invoking the code generator *}
+
+subsection {* Selecting code equations *}
+
+text {* inspection by @{text "code_thms"} *}
+
+subsection {* The preprocessor *}
+
+subsection {* Datatypes *}
+
+text {* example: @{text "rat"}, cases *}
+
+subsection {* Equality and wellsortedness *}
+
+subsection {* Partiality *}
+
+text {* @{text "code_abort"}, examples: maps *}
+
+end
--- a/doc-src/IsarAdvanced/Codegen/Thy/ROOT.ML Fri Sep 12 12:04:20 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/ROOT.ML Sun Sep 14 21:50:35 2008 +0200
@@ -2,3 +2,11 @@
(* $Id$ *)
use_thy "Codegen";
+
+(*no_document use_thy "Setup";
+
+use_thy "Introduction";
+use_thy "Program";
+use_thy "Adaption";
+use_thy "Further";
+use_thy "ML";*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Setup.thy Sun Sep 14 21:50:35 2008 +0200
@@ -0,0 +1,8 @@
+theory Setup
+imports Main
+uses "../../../antiquote_setup.ML"
+begin
+
+ML_val {* Code_Target.code_width := 74 *}
+
+end
--- a/doc-src/IsarAdvanced/Codegen/codegen.tex Fri Sep 12 12:04:20 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/codegen.tex Sun Sep 14 21:50:35 2008 +0200
@@ -80,10 +80,9 @@
\maketitle
\begin{abstract}
- This tutorial gives a motivation-driven introduction
- to a generic code generator framework in Isabelle
- for generating executable code in functional
- programming languages from logical specifications.
+ This tutorial gives am introduction to a generic code generator framework in Isabelle
+ for generating executable code in functional programming languages from logical
+ specifications in Isabelle/HOL.
\end{abstract}
\thispagestyle{empty}\clearpage
@@ -92,6 +91,11 @@
\clearfirst
\input{Thy/document/Codegen.tex}
+% \input{Thy/document/Introduction.tex}
+% \input{Thy/document/Program.tex}
+% \input{Thy/document/Adaption.tex}
+% \input{Thy/document/Further.tex}
+% \input{Thy/document/ML.tex}
\begingroup
%\tocentry{\bibname}