1.1 --- a/src/Tools/isac/Interpret/script.sml	Tue May 17 17:54:58 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Wed May 18 08:47:10 2011 +0200
     1.3 @@ -1751,14 +1751,17 @@
     1.4  
     1.5  (*.get script and istate from PblObj, see                        (*1*) above.*)
     1.6  fun from_pblobj' thy' (p,p_) pt =
     1.7 -    let val p' = par_pblobj pt p
     1.8 -	val thy = assoc_thy thy'
     1.9 -	val PblObj{meth=itms,...} = get_obj I pt p'
    1.10 -	val metID = get_obj g_metID pt p'
    1.11 -	val {srls,scr,...} = get_met metID
    1.12 -    in if last_elem p = 0 (*nothing written to pt yet*)
    1.13 -       then let val (is, ctxt, scr) = init_scrstate thy itms metID
    1.14 -	    in (srls, (is, ctxt), scr) end
    1.15 +  let
    1.16 +    val p' = par_pblobj pt p
    1.17 +	  val thy = assoc_thy thy'
    1.18 +	  val PblObj {meth=itms, ctxt, ...} = get_obj I pt p'
    1.19 +	  val metID = get_obj g_metID pt p'
    1.20 +	  val {srls,scr,...} = get_met metID
    1.21 +  in
    1.22 +    if last_elem p = 0 (*nothing written to pt yet*)
    1.23 +    then
    1.24 +       let val (is, _, scr) = init_scrstate thy itms metID
    1.25 +	     in (srls, (is, ctxt), scr) end
    1.26         else (srls, get_loc pt (p,p_), scr)
    1.27      end;
    1.28