src/HOL/Tools/watcher.ML
changeset 24425 ca97c6f3d9cd
parent 24386 7cbaf94aed08
child 24584 01e83ffa6c54
     1.1 --- a/src/HOL/Tools/watcher.ML	Fri Aug 24 14:15:58 2007 +0200
     1.2 +++ b/src/HOL/Tools/watcher.ML	Fri Aug 24 14:16:44 2007 +0200
     1.3 @@ -360,12 +360,14 @@
     1.4  
     1.5  (*Successful outcome: auto-insertion of commands into the PG buffer. Thanks to D Aspinall!!*)
     1.6  fun report_success i s sgtx = 
     1.7 -  let val lines = String.tokens (fn c => c = #"\n") s
     1.8 -  in  if length lines > 1 then report i (s ^ sgtx)  (*multiple commands: do the old way*)
     1.9 -      else priority (cat_lines ["Subgoal " ^ string_of_int i ^ ":", sgtx,
    1.10 -                                "  Try this command:", Markup.enclose Markup.sendback s])
    1.11 -  end;
    1.12 -
    1.13 +  let val sgline = "Subgoal " ^ string_of_int i ^ ":"
    1.14 +      val outlines = 
    1.15 +	case split_lines s of
    1.16 +	    [] => ["Received bad string: " ^ s]
    1.17 +	  | line::lines => ["  Try this command:", (*Markup.enclose Markup.sendback*) line, ""]
    1.18 +	                   @ lines
    1.19 +  in priority (cat_lines (sgline::sgtx::outlines)) end;
    1.20 +  
    1.21  fun createWatcher (ctxt, th, thm_names_list) =
    1.22   let val {pid=childpid, instr=childin, outstr=childout} = setupWatcher (ctxt,th,thm_names_list)
    1.23       fun decr_watched() =