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