- if success then
- gui#lockScript (locked_iter#offset + interpreter#endOffset)
-
-let script_jump _ =
- let buf = gui#script#scriptTextView#buffer in
- let locked_iter = buf#get_iter_at_mark (`NAME "locked") in
- let cursor_iter = buf#get_iter_at_mark (`NAME "insert") in
- let raw_text = buf#get_text ~start:locked_iter ~stop:cursor_iter () in
- let len = String.length raw_text in
- let rec parse offset =
- if offset < len then begin
- let (success, hide) =
- interpreter#evalPhrase (String.sub raw_text offset (len - offset))
- in
- if success then begin
- let new_offset = interpreter#endOffset + offset in
- gui#lockScript (new_offset + locked_iter#offset);
- parse new_offset
- end else
- raise Exit
- end
+ let needed_by_script ast =
+ match strip_locations ast with
+ | A.Tactic _
+ | A.Command
+ (A.Inductive _ | A.Theorem _ | A.Coercion _ | A.Qed _ | A.Proof) ->
+ true
+ | _ -> false