- (** prompt the user for the textual input of a term and disambiguate it *)
-let ask_term ?(title = "term input") ?(msg = "insert term") () =
- match gui#askText ~title ~msg () with
- | Some t ->
- let (_, _, term) = disambiguator#disambiguateTerm (Stream.of_string t) in
- Some term
- | None -> None
+(** {2 Script window handling} *)
+
+let script_forward _ =
+ let buf = gui#script#scriptTextView#buffer in
+ let locked_iter = buf#get_iter_at_mark (`NAME "locked") in
+ if
+ interpreter#evalPhrase
+ (buf#get_text ~start:locked_iter ~stop:buf#end_iter ());
+ 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
+ if
+ interpreter#evalPhrase ~transparent:true
+ (String.sub raw_text offset (len - offset));
+ then begin
+ let new_offset = interpreter#endOffset + offset in
+ gui#lockScript (new_offset + locked_iter#offset);
+ parse new_offset
+ end else
+ raise Exit
+ end
+ in
+ try
+ parse 0
+ with Exit -> ()
+
+let script_back _ = not_implemented "script_back"
+
+let load_script fname =
+ gui#script#scriptTextView#buffer#set_text (input_file fname);
+ gui#script#scriptWin#show ();
+ gui#main#showScriptMenuItem#set_active true
+
+(** {2 GUI callbacks} *)