# HG changeset patch # User wenzelm # Date 1196896890 -3600 # Node ID 87d89b0f847a5dfd96fadfb688c4eac45324bbd4 # Parent c482262dd960e9c5eeee208678697261ec1e7e41 replaced Markup.enclose by Markup.markup, which operates on plain strings instead of raw output; diff -r c482262dd960 -r 87d89b0f847a src/HOL/Tools/watcher.ML --- a/src/HOL/Tools/watcher.ML Thu Dec 06 00:21:28 2007 +0100 +++ b/src/HOL/Tools/watcher.ML Thu Dec 06 00:21:30 2007 +0100 @@ -364,7 +364,7 @@ val outlines = case split_lines s of [] => ["Received bad string: " ^ s] - | line::lines => [" Try this command:", (*Markup.enclose Markup.sendback*) line, ""] + | line::lines => [" Try this command:", (*Markup.markup Markup.sendback*) line, ""] @ lines in priority (cat_lines (sgline::sgtx::outlines)) end; diff -r c482262dd960 -r 87d89b0f847a src/Pure/General/position.ML --- a/src/Pure/General/position.ML Thu Dec 06 00:21:28 2007 +0100 +++ b/src/Pure/General/position.ML Thu Dec 06 00:21:30 2007 +0100 @@ -66,6 +66,6 @@ fun str_of (Pos (NONE, NONE)) = "" | str_of pos = - " " ^ Markup.enclose (Markup.properties (properties_of pos) Markup.position) (print pos); + " " ^ Markup.markup (Markup.properties (properties_of pos) Markup.position) (print pos); end; diff -r c482262dd960 -r 87d89b0f847a src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Thu Dec 06 00:21:28 2007 +0100 +++ b/src/Pure/Isar/toplevel.ML Thu Dec 06 00:21:30 2007 +0100 @@ -762,7 +762,7 @@ let fun check_secure () = (if secure then warning "Secure loop -- cannot exit to ML" else (); secure); - val prompt = Output.escape (Markup.enclose Markup.prompt Source.default_prompt); + val prompt = Markup.markup Markup.prompt Source.default_prompt; in (case get_interrupt (Source.set_prompt prompt src) of NONE => (writeln "\nInterrupt."; raw_loop secure src)