5 (* rebuilding the output function from ThyOutput in order to *)

     5 (* rebuilding the output function from ThyOutput in order to *)

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

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

     7 

     7 

     8 val gray = ref false

     8 val gray = ref false

     9 val linenos = ref false

     9 val linenos = ref false

    10 

    11 

    11 fun output txt =

    12 fun output txt =

    12 let

    13 let

    13   val prts = map Pretty.str txt

    14   val prts = map Pretty.str txt

    14 in   

    15 in   

    23   else

    24   else

    24     map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of))

    25     map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of))

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

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

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

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

    27 end

    28 end

    29 

    29 

    30 datatype qstring =

    30 datatype qstring =

    31   NoString

    31   NoString

    32 | Plain   of string

    32 | Plain   of string

    33 | Code    of string

    33 | Code    of string