# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1257253023 -3600
# Node ID 28a49fe024c97a64c357842b95230dce4b91f51a
# Parent  6bf955db9b623d82517e78ca1d2250aa7c2c482f
added structure index

diff -r 6bf955db9b62 -r 28a49fe024c9 IsaMakefile
--- a/IsaMakefile	Tue Nov 03 07:10:05 2009 +0100
+++ b/IsaMakefile	Tue Nov 03 13:57:03 2009 +0100
@@ -27,6 +27,9 @@
 	$(ISABELLE_TOOL) version > ProgTutorial/generated/version 
 	$(ML_HOME)/poly -v > ProgTutorial/generated/pversion
 	$(ISABELLE_TOOL) document -o pdf  ProgTutorial/generated
+	makeindex -o ProgTutorial/generated/root.stu ProgTutorial/generated/root.str
+	$(ISABELLE_TOOL) document -o pdf  ProgTutorial/generated
+##	$(ISABELLE_TOOL) document -o pdf  ProgTutorial/generated
 	@cp ProgTutorial/document.pdf progtutorial.pdf
 
 ## clean
diff -r 6bf955db9b62 -r 28a49fe024c9 ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Tue Nov 03 07:10:05 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Tue Nov 03 13:57:03 2009 +0100
@@ -404,7 +404,7 @@
   comprehension of the code, but after getting familiar with them, they
   actually ease the understanding and also the programming.
 
-  The simplest combinator is @{ML_ind I in Basic_Library}, which is just the 
+  The simplest combinator is @{ML_ind I in Library}, which is just the 
   identity function defined as
 *}
 
diff -r 6bf955db9b62 -r 28a49fe024c9 ProgTutorial/document/root.tex
--- a/ProgTutorial/document/root.tex	Tue Nov 03 07:10:05 2009 +0100
+++ b/ProgTutorial/document/root.tex	Tue Nov 03 13:57:03 2009 +0100
@@ -14,7 +14,6 @@
 \usepackage{boxedminipage}
 \usepackage{mathpartir}
 \usepackage{flafter}
-\usepackage{makeidx}
 \usepackage{index}
 \usepackage{tocbibind}
 \usepackage{tikz}
@@ -30,7 +29,8 @@
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % indexing
-\makeindex
+\newindex{default}{idx}{ind}{Index}
+\newindex{str}{str}{stu}{Structure Index}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % For cross references to the other manuals:
@@ -180,7 +180,10 @@
 \bibliographystyle{abbrv}
 \bibliography{root}
 
-% index
+% indices
+\setindexname{Structure Index}
+\printindex[str]
+\setindexname{Index}
 \printindex
 
 \end{document}
diff -r 6bf955db9b62 -r 28a49fe024c9 ProgTutorial/output_tutorial.ML
--- a/ProgTutorial/output_tutorial.ML	Tue Nov 03 07:10:05 2009 +0100
+++ b/ProgTutorial/output_tutorial.ML	Tue Nov 03 13:57:03 2009 +0100
@@ -69,9 +69,15 @@
   then implode ["\\index{", get_indstring m, "}"]  
   else implode ["\\index{", get_indstring m, " (", get_indstring n, ")}"])  
     
+fun get_str_index {main = m, minor = n} = 
+ (case n of
+   Struct s => implode ["\\index[str]{{\\tt\\slshape{}", get_word s, "}!", get_indstring m, "}"]
+  | _ => "")
+
 fun output_indexed ind txt =
  txt |> output
      |> prefix (get_index ind)
+     |> prefix (get_str_index ind)
 
 fun boolean "" = true
   | boolean "true" = true
diff -r 6bf955db9b62 -r 28a49fe024c9 progtutorial.pdf
Binary file progtutorial.pdf has changed