src/Pure/PIDE/command.ML
changeset 68344 3bb44c25ce8b
parent 68334 ed40728c45d0
child 68366 cd387c55e085
     1.1 --- a/src/Pure/PIDE/command.ML	Thu May 31 22:59:08 2018 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Fri Jun 01 10:56:01 2018 +0200
     1.3 @@ -22,10 +22,10 @@
     1.4    val eval: Keyword.keywords -> Path.T -> (unit -> theory) ->
     1.5      blob list * int -> Document_ID.command -> Token.T list -> eval -> eval
     1.6    type print
     1.7 -  val print0: (unit -> unit) -> eval -> print
     1.8 +  type print_fn = Toplevel.transition -> Toplevel.state -> unit
     1.9 +  val print0: {pri: int, print_fn: print_fn} -> eval -> print
    1.10    val print: bool -> (string * string list) list -> Keyword.keywords -> string ->
    1.11      eval -> print list -> print list option
    1.12 -  type print_fn = Toplevel.transition -> Toplevel.state -> unit
    1.13    type print_function =
    1.14      {keywords: Keyword.keywords, command_name: string, args: string list, exec_id: Document_ID.exec} ->
    1.15        {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option
    1.16 @@ -342,9 +342,9 @@
    1.17  
    1.18  in
    1.19  
    1.20 -fun print0 e =
    1.21 +fun print0 {pri, print_fn} =
    1.22    make_print ("", [serial_string ()])
    1.23 -    {delay = NONE, pri = 0, persistent = true, strict = true, print_fn = fn _ => fn _ => e ()};
    1.24 +    {delay = NONE, pri = pri, persistent = true, strict = true, print_fn = print_fn};
    1.25  
    1.26  fun print command_visible command_overlays keywords command_name eval old_prints =
    1.27    let