structure OutputTutorial =
struct

(* rebuilding the output function from Thy_Output in order to *)
(* enable the options [gray, linenos]                        *)

val gray = Unsynchronized.ref false
val linenos = Unsynchronized.ref false


fun output ctxt txt =
let
  val prts = map Pretty.str txt
in   
  prts
  |> (if Config.get ctxt Thy_Output.quotes then map Pretty.quote else I)
  |> (if Config.get ctxt Thy_Output.display then
    map (Output.output o Pretty.string_of o Pretty.indent (Config.get ctxt Thy_Output.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 Config.get ctxt Thy_Output.break then Pretty.string_of else Pretty.str_of))
    #> space_implode "\\isasep\\isanewline%\n"
    #> enclose "\\isa{" "}")
end

datatype indstring =
  NoString
| Plain   of string
| Code    of string
| Struct  of string

fun translate_string f = Symbol.explode #> map f #> implode;

val clean_string = translate_string
  (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 ("Only single word allowed! Error with " ^ quote str)
end  

fun get_indstring NoString = ""
  | get_indstring (Plain s) = get_word s
  | get_indstring (Code s) = let val w = get_word s in implode[w, "@{\\tt\\slshape{}", w, "}"] end
  | get_indstring (Struct s) =  implode ["in {\\tt\\slshape{}", get_word s, "}"]

fun get_index {main = m, minor = n} = 
 (if n = NoString
  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 ctxt ind txt =
 txt |> output ctxt
     |> prefix (get_index ind)
     |> prefix (get_str_index ind)

fun boolean "" = true
  | boolean "true" = true
  | boolean "false" = false
  | boolean s = error ("Bad boolean value: " ^ quote s);

val gray_setup = Thy_Output.add_option @{binding "gray"} 
  (Thy_Output.add_wrapper o Library.setmp_CRITICAL gray o boolean)
val linenos_setup = Thy_Output.add_option @{binding "linenos"}  
  (Thy_Output.add_wrapper o Library.setmp_CRITICAL linenos o boolean)

val setup =
  gray_setup #>
  linenos_setup 

end