--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ProgTutorial/output_tutorial.ML	Sat May 30 17:40:20 2009 +0200
@@ -0,0 +1,101 @@
+
+structure OutputTutorial =
+struct
+
+(* rebuilding the output function from ThyOutput in order to *)
+(* enable the options [gray, linenos, index]                   *)
+
+val gray = ref false
+val linenos = ref false
+
+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}"
+  else
+    map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of))
+    #> space_implode "\\isasep\\isanewline%\n"
+    #> enclose "\\isa{" "}")
+end
+
+datatype qstring =
+  Plain of string
+| Code  of string
+
+datatype entry = 
+   No_Entry
+ | Default 
+ | Explicit of string
+
+val index = ref No_Entry
+
+fun translate f = Symbol.explode #> map f #> implode;
+
+val clean_string = translate
+  (fn "_" => "\\_"
+    | "#" => "\\#"
+    | "<" => "\\isacharless"
+    | ">" => "\\isachargreater"
+    | "{" => "\\{"
+    | "|" => "\\isacharbar"
+    | "}" => "\\}"
+    | "$" => "\\isachardollar"
+    | "!" => "\\isacharbang"
+    | "\\<dash>" => "-"
+    | c => c);
+
+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 (clean_string str)
+  else error ("Underspecified index entry only for single words allowed! Error with " ^ quote str)
+end  
+
+fun get_qstring (Plain s) = get_word s
+  | get_qstring (Code s) = let val w = get_word s in  (w ^ "@{\\tt\\slshape{}" ^ w ^ "}") end
+
+fun is_empty_qstr (Plain "") = true
+  | is_empty_qstr (Code "") = true
+  | is_empty_qstr _ = false
+
+fun get_index_info {main = m, minor = n} = 
+ (if n = ""
+  then "\\index{" ^ (get_qstring m) ^ "}"  
+  else "\\indexdef{" ^ (get_qstring m) ^ "}{" ^ n ^ "}")  
+    
+fun index_entry entry index_info  =
+ case entry of
+   No_Entry => I
+ | Explicit s => prefix s
+ | Default => prefix (get_index_info index_info)
+
+fun output_indexed txt index_info =
+ txt |> output
+     |> index_entry (!index) index_info
+
+fun boolean "" = true
+  | boolean "true" = true
+  | boolean "false" = false
+  | boolean s = error ("Bad boolean value: " ^ quote s);
+
+fun explicit "" = Default
+  | explicit s  = Explicit s
+
+val _ = ThyOutput.add_options
+ [("gray", Library.setmp gray o boolean),
+  ("linenos", Library.setmp linenos o boolean),
+  ("index", Library.setmp index o explicit)]
+
+
+end
\ No newline at end of file