structure OutputTutorial =

struct

(* rebuilding the output function from Thy_Output in order to *)

(* enable the options [gray, linenos]                        *)

val thy_output_linenos = Attrib.setup_config_bool @{binding linenos} (K false)

val thy_output_gray = Attrib.setup_config_bool @{binding gray} (K false)

fun output_raw ctxt txt =

let

  val prts = map Pretty.str txt

in   

  prts

  |> (if Config.get ctxt Document_Antiquotation.thy_output_quotes then map Pretty.quote else I)

  |> (if Config.get ctxt Document_Antiquotation.thy_output_display then

    map (Output.output o Pretty.string_of o Pretty.indent (Config.get ctxt Document_Antiquotation.thy_output_indent))

    #> space_implode "\\isasep\\isanewline%\n"

    #> (if Config.get ctxt thy_output_linenos then (enclose "\\begin{linenos}%\n" "%\n\\end{linenos}") else I) 

    #> (if  Config.get ctxt thy_output_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 Document_Antiquotation.thy_output_break then Pretty.string_of else Pretty.unformatted_string_of))

    #> space_implode "\\isasep\\isanewline%\n"

    #> enclose "\\isa{" "}")

end

fun output ctxt txt = Latex.string (output_raw ctxt txt)

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_raw ctxt

     |> prefix (get_index ind)

     |> prefix (get_str_index ind)

     |> Latex.string

fun boolean "" = true

  | boolean "true" = true

  | boolean "false" = false

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

val _ = Theory.setup 

  (Document_Antiquotation.setup_option @{binding gray} (Config.put thy_output_gray o boolean) #> 

   Document_Antiquotation.setup_option @{binding linenos} (Config.put thy_output_linenos o boolean) ); 

end