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 =

  NoString

| Plain   of string

| Code    of string

| IStruct 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 NoString = ""

  | get_qstring (Plain s) = get_word s

  | get_qstring (Code s) = let val w = get_word s in  (w ^ "@{\\tt\\slshape{}" ^ w ^ "}") end

  | get_qstring (IStruct s) =  "in {\\tt\\slshape{}" ^ (get_word s) ^ "}"

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 = NoString

  then "\\index{" ^ (get_qstring m) ^ "}"  

  else "\\indexdef{" ^ (get_qstring m) ^ "}{" ^ (get_qstring 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