# HG changeset patch
# User wenzelm
# Date 1199631474 -3600
# Node ID 713519ba6860a82b9f35adf32fd1efccc922e27e
# Parent  f5fb187ae10d54ab05cfb114d58acb631d02498c
removed obsolete prompt markup;

diff -r f5fb187ae10d -r 713519ba6860 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sun Jan 06 15:57:52 2008 +0100
+++ b/src/Pure/Isar/toplevel.ML	Sun Jan 06 15:57:54 2008 +0100
@@ -786,9 +786,8 @@
   let
     fun check_secure () =
       (if secure then warning "Secure loop -- cannot exit to ML" else (); secure);
-    val prompt = Markup.markup Markup.prompt Source.default_prompt;
   in
-    (case get_interrupt (Source.set_prompt prompt src) of
+    (case get_interrupt (Source.set_prompt Source.default_prompt src) of
       NONE => (writeln "\nInterrupt."; raw_loop secure src)
     | SOME NONE => if secure then quit () else ()
     | SOME (SOME (tr, src')) => if >> tr orelse check_secure () then raw_loop secure src' else ())
diff -r f5fb187ae10d -r 713519ba6860 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Jan 06 15:57:52 2008 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Jan 06 15:57:54 2008 +0100
@@ -305,8 +305,7 @@
    else if name = Markup.typN      then typ_markup markup
    else if name = Markup.termN     then term_markup markup
    else if name = Markup.keywordN  then keyword_markup markup
-   else if name = Markup.commandN  then command_markup markup 
-   else if name = Markup.promptN   then prompt_markup markup *)
+   else if name = Markup.commandN  then command_markup markup*)
    else if name = Markup.stateN    then state_markup
 (* else if name = Markup.subgoalN  then subgoal_markup () *)
    else ("", "");