src/Pure/Isar/toplevel.ML

 fun warn_secure () =
   let val secure = Secure.is_secure ()
   in if secure then warning "Cannot exit to ML in secure mode" else (); secure end;
 
 fun raw_loop src =
-  let val prompt =
-    Output.escape ((Markup.output Markup.prompt |-> enclose) Source.default_prompt)
-  in
+  let val prompt = Output.escape (Markup.enclose Markup.prompt Source.default_prompt) in
     (case get_interrupt (Source.set_prompt prompt src) of
       NONE => (writeln "\nInterrupt."; raw_loop src)
     | SOME NONE => if warn_secure () then quit () else ()
     | SOME (SOME (tr, src')) =>
         if >> tr orelse warn_secure () then raw_loop src'