equal
deleted
inserted
replaced
419 fun apply_text current_context text state = |
419 fun apply_text current_context text state = |
420 let |
420 let |
421 val ctxt = context_of state; |
421 val ctxt = context_of state; |
422 |
422 |
423 fun eval (Method.Basic m) = apply_method current_context m |
423 fun eval (Method.Basic m) = apply_method current_context m |
424 | eval (Method.Source src) = |
424 | eval (Method.Source src) = apply_method current_context (Method.method_cmd ctxt src) |
425 apply_method current_context (Method.the_method ctxt (Method.check_source ctxt src)) |
|
426 | eval (Method.Then (_, txts)) = Seq.EVERY (map eval txts) |
425 | eval (Method.Then (_, txts)) = Seq.EVERY (map eval txts) |
427 | eval (Method.Orelse (_, txts)) = Seq.FIRST (map eval txts) |
426 | eval (Method.Orelse (_, txts)) = Seq.FIRST (map eval txts) |
428 | eval (Method.Try (_, txt)) = Seq.TRY (eval txt) |
427 | eval (Method.Try (_, txt)) = Seq.TRY (eval txt) |
429 | eval (Method.Repeat1 (_, txt)) = Seq.REPEAT1 (eval txt) |
428 | eval (Method.Repeat1 (_, txt)) = Seq.REPEAT1 (eval txt) |
430 | eval (Method.Select_Goals (_, n, txt)) = select_goals n (eval txt); |
429 | eval (Method.Select_Goals (_, n, txt)) = select_goals n (eval txt); |