diff -r ef1da1abee46 -r 1fb8d62c88a0 ProgTutorial/outputfn.ML
--- a/ProgTutorial/outputfn.ML	Sat May 30 11:12:46 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,79 +0,0 @@
-
-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