src/Pure/Thy/thy_output.ML
changeset 23863 8f3099589cfa
parent 23725 1f84af8b2e71
child 23935 2a4e42ec9a54
     1.1 --- a/src/Pure/Thy/thy_output.ML	Thu Jul 19 23:18:46 2007 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Thu Jul 19 23:18:48 2007 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4    datatype markup = Markup | MarkupEnv | Verbatim
     1.5    val modes: string list ref
     1.6    val eval_antiquote: Scan.lexicon -> Toplevel.node option -> string * Position.T -> string
     1.7 -  val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
     1.8 +  val process_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
     1.9      Toplevel.transition list -> (OuterLex.token, 'a) Source.source -> Buffer.T
    1.10    val output_list: (Proof.context -> 'a -> Pretty.T) -> Args.src ->
    1.11      Proof.context -> 'a list -> string
    1.12 @@ -286,7 +286,7 @@
    1.13  end;
    1.14  
    1.15  
    1.16 -(* present_thy *)
    1.17 +(* process_thy *)
    1.18  
    1.19  datatype markup = Markup | MarkupEnv | Verbatim;
    1.20  
    1.21 @@ -317,7 +317,7 @@
    1.22  
    1.23  in
    1.24  
    1.25 -fun present_thy lex default_tags is_markup trs src =
    1.26 +fun process_thy lex default_tags is_markup trs src =
    1.27    let
    1.28      (* tokens *)
    1.29