--- a/ProgTutorial/Base.thy	Fri May 29 12:15:48 2009 +0200
+++ b/ProgTutorial/Base.thy	Sat May 30 11:12:46 2009 +0200
@@ -1,6 +1,7 @@
 theory Base
 imports Main
 uses
+  "outputfn.ML"
   "chunks.ML"
   "antiquote_setup.ML"
 begin
@@ -37,4 +38,5 @@
 
 *}
 
+
 end
\ No newline at end of file

--- a/ProgTutorial/FirstSteps.thy	Fri May 29 12:15:48 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Sat May 30 11:12:46 2009 +0200
@@ -4,6 +4,7 @@
 
 chapter {* First Steps *}
 
+
 text {*
   Isabelle programming is done in ML. Just like lemmas and proofs, ML-code
   in Isabelle is part of a theory. If you want to follow the code given in
@@ -110,7 +111,7 @@
 
   During development you might find it necessary to inspect some data
   in your code. This can be done in a ``quick-and-dirty'' fashion using 
-  the function @{ML "writeln"}. For example 
+  the function @{ML [indexc] "writeln"}. For example 
 
   @{ML_response_fake [display,gray] "writeln \"any string\"" "\"any string\""}
 
@@ -716,6 +717,7 @@
   "x x"}
 
   with the raw ML-constructors.
+  
   Sometimes the internal representation of terms can be surprisingly different
   from what you see at the user-level, because the layers of
   parsing/type-checking/pretty printing can be quite elaborate. 
@@ -781,7 +783,7 @@
   \end{readmore}
 *}
 
-section {* Constructing Terms and Types Manually\label{sec:terms_types_manually} *} 
+section {* Constructing Terms Manually\label{sec:terms_types_manually} *} 
 
 text {*
   While antiquotations are very convenient for constructing terms, they can
@@ -877,6 +879,16 @@
   @{term \"(\<lambda>x::nat. x)\"}"
   "Free (\"x\", \"nat\")"}
 
+  There are many convenient functions that construct specific HOL-terms. For
+  example @{ML "HOLogic.mk_eq"} constructs an equality out of two terms.
+  The types needed in this equality are calculated from the type of the
+  arguments. For example
+
+@{ML_response_fake [gray,display]
+  "writeln (Syntax.string_of_term @{context}
+   (HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"})))"
+  "True = False"}
+
   \begin{readmore}
   There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and
   @{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms 
@@ -897,7 +909,11 @@
   in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produces the
   number representing their sum.
   \end{exercise}
-
+*}
+
+section {* Constants *}
+
+text {*
   There are a few subtle issues with constants. They usually crop up when
   pattern matching terms or types, or when constructing them. While it is perfectly ok
   to write the function @{text is_true} as follows
@@ -1003,7 +1019,11 @@
   Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"};
   functions about signatures in @{ML_file "Pure/sign.ML"}.
   \end{readmore}
-
+*}
+
+section {* Constructing Types Manually *}
+
+text {*
   Although types of terms can often be inferred, there are many
   situations where you need to construct types manually, especially  
   when defining constants. For example the function returning a function 
@@ -1018,6 +1038,13 @@
 ML{*fun make_fun_type ty1 ty2 = ty1 --> ty2 *}
 
 text {*
+  If you want to construct a function type with more than one argument
+  type, then you can use @{ML "--->"}.
+*}
+
+ML{*fun make_fun_types tys ty = tys ---> ty *}
+
+text {*
   A handy function for manipulating terms is @{ML map_types}: it takes a 
   function and applies it to every type in a term. You can, for example,
   change every @{typ nat} in a term into an @{typ int} using the function:
@@ -1551,7 +1578,7 @@
   @{text GenericDataFun}:
 *}
 
-ML {*structure MyThmsData = GenericDataFun
+ML{*structure MyThmsData = GenericDataFun
  (type T = thm list
   val empty = []
   val extend = I

--- a/ProgTutorial/Tactical.thy	Fri May 29 12:15:48 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Sat May 30 11:12:46 2009 +0200
@@ -694,7 +694,7 @@
   quantified variable. So you really have to construct the pattern using the
   basic term-constructors. This is not necessary in other cases, because their
   type is always fixed to function types involving only the type @{typ
-  bool}. (See Section \ref{sec:terms_types_manually} about constructing terms
+  bool}. (See Section \ref{sec:terms_manually} about constructing terms
   manually.) For the catch-all pattern, we chose to just return @{ML all_tac}. 
   Consequently, @{ML select_tac} never fails.
 

--- a/ProgTutorial/antiquote_setup.ML	Fri May 29 12:15:48 2009 +0200
+++ b/ProgTutorial/antiquote_setup.ML	Sat May 30 11:12:46 2009 +0200
@@ -40,7 +40,7 @@
   #> string_explode "";
 
 (* output function *)
-fun output_fn txt =  Chunks.output (map Pretty.str txt)
+fun output_fn txt =  OutputFN.output txt
 
 (* checks and prints open expressions *)
 fun output_ml {context = ctxt, ...} (txt, ovars) =

--- a/ProgTutorial/chunks.ML	Fri May 29 12:15:48 2009 +0200
+++ b/ProgTutorial/chunks.ML	Sat May 30 11:12:46 2009 +0200
@@ -2,39 +2,6 @@
 structure Chunks =
 struct
 
-(* rebuilding the output function from ThyOutput in order to *)
-(* enable the options [gray, linenos]                        *)
-
-val gray = ref false;
-val linenos = ref false
-
-fun output prts =
-  prts
-  |> (if ! ThyOutput.quotes then map Pretty.quote else I)
-  |> (if ! ThyOutput.display then
-    map (Output.output o Pretty.string_of o Pretty.indent (! ThyOutput.indent))
-    #> space_implode "\\isasep\\isanewline%\n"
-    #> (if ! linenos then (enclose "\\begin{linenos}%\n" "%\n\\end{linenos}") else I) 
-    #> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I) 
-    #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
-  else
-    map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of))
-    #> space_implode "\\isasep\\isanewline%\n"
-    #> enclose "\\isa{" "}");
-
-
-fun boolean "" = true
-  | boolean "true" = true
-  | boolean "false" = false
-  | boolean s = error ("Bad boolean value: " ^ quote s);
-
-val _ = ThyOutput.add_options
- [("gray", Library.setmp gray o boolean),
-  ("linenos", Library.setmp linenos o boolean)]
-
-
-
-
 (** theory data **)
 
 structure ChunkData = TheoryDataFun
@@ -158,8 +125,7 @@
           end)
     val txt = spc ^ implode (transform_cmts toks')
   in
-    txt |> split_lines |>
-    (map Pretty.str) |> output 
+    txt |> split_lines |> OutputFN.output 
   end;
 
 val _ = ThyOutput.antiquotation "ML_chunk" (Scan.lift Args.name) output_chunk;

--- a/ProgTutorial/document/root.tex	Fri May 29 12:15:48 2009 +0200
+++ b/ProgTutorial/document/root.tex	Sat May 30 11:12:46 2009 +0200
@@ -1,4 +1,4 @@
-\documentclass[11pt,a4paper]{report}
+\documentclass[11pt,a4paper]{book}
 \usepackage[latin1]{inputenc}
 \usepackage{amsmath,amsthm}
 \usepackage{isabelle}
@@ -15,6 +15,7 @@
 \usepackage{boxedminipage}
 \usepackage{mathpartir}
 \usepackage{flafter}
+\usepackage{makeidx}
 \usepackage{pdfsetup}
 
 \urlstyle{rm}
@@ -24,6 +25,14 @@
 \isadroptag{theory}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% adding chapters explicitly to the table of content
+\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% indexing
+\makeindex
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % For cross references to the other manuals:
 \usepackage{xr}
 \externaldocument[I-]{implementation}
@@ -149,16 +158,24 @@
         \end{tabular}}
 
 \maketitle
+
+% table of contents
+\tocentry{\contentsname}
 \setcounter{tocdepth}{1}
 \tableofcontents
 
 % generated text of all theories
 \input{session}
 
-\newpage
+% bibliography
+\tocentry{\bibname}
 \bibliographystyle{abbrv}
 \bibliography{root}
 
+% index
+\tocentry{\indexname}
+\printindex
+
 \end{document}
 
 %%% Local Variables:

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ProgTutorial/outputfn.ML	Sat May 30 11:12:46 2009 +0200
@@ -0,0 +1,79 @@
+
+structure OutputFN =
+struct
+
+(* rebuilding the output function from ThyOutput in order to *)
+(* enable the options [gray, linenos, index]                   *)
+
+val gray = ref false
+val linenos = ref false
+
+datatype entry = 
+   No_Entry
+ | Code_Entry of string
+ | String_Entry of string
+
+val index = ref No_Entry
+
+fun string_entry s = prefix ("\\index{" ^ s ^ "}")
+fun code_entry   s = prefix ("\\index{" ^ s ^ "@{\\tt\\slshape{}" ^ s ^ "}}")
+
+fun get_word str =
+let 
+  fun only_letters [] = true
+    | only_letters (x::xs) = 
+        if (Symbol.is_ascii_blank x) then false else only_letters xs
+in
+  if (only_letters (Symbol.explode str)) then str
+  else error ("Underspecified index entry only for single words allowed! Error with " ^ str)
+end  
+    
+fun index_entry entry txt =
+ case entry of
+   No_Entry => I
+ | String_Entry "" => string_entry (get_word (implode txt))
+ | String_Entry s  => string_entry s
+ | Code_Entry ""   => code_entry (get_word (implode txt))
+ | Code_Entry s    => code_entry s
+
+
+fun translate f = Symbol.explode #> map f #> implode;
+
+val clean_string = translate
+  (fn "_" => "\\_"
+    | c => c);
+
+fun output txt =
+let
+  val prts = map Pretty.str txt
+in   
+  prts
+  |> (if ! ThyOutput.quotes then map Pretty.quote else I)
+  |> (if ! ThyOutput.display then
+    map (Output.output o Pretty.string_of o Pretty.indent (! ThyOutput.indent))
+    #> space_implode "\\isasep\\isanewline%\n"
+    #> (if ! linenos then (enclose "\\begin{linenos}%\n" "%\n\\end{linenos}") else I) 
+    #> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I) 
+    #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
+    #> index_entry (!index) txt
+  else
+    map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of))
+    #> space_implode "\\isasep\\isanewline%\n"
+    #> enclose "\\isa{" "}"
+    #> index_entry (!index) txt)
+end
+
+
+fun boolean "" = true
+  | boolean "true" = true
+  | boolean "false" = false
+  | boolean s = error ("Bad boolean value: " ^ quote s);
+
+val _ = ThyOutput.add_options
+ [("gray", Library.setmp gray o boolean),
+  ("linenos", Library.setmp linenos o boolean),
+  ("index", Library.setmp index o String_Entry o clean_string),
+  ("indexc", Library.setmp index o Code_Entry o clean_string)]
+
+
+end
\ No newline at end of file

Binary file progtutorial.pdf has changed