let t_and_ty = Cic.Cast (term,ty) in
guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv));
[], "", parsed_text_length
- | TA.Inline (_,suri) ->
+ | TA.Inline (_,style,suri,prefix) ->
let dbd = LibraryDb.instance () in
let uris =
let sql_pat =
(fun uri ->
prerr_endline ("Stampo " ^ UriManager.string_of_uri uri);
try
- ObjPp.obj_to_string 80
+ ObjPp.obj_to_string 78 style prefix (* FG: mi pare meglio 78 *)
(fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri))
with
- _ (* BRRRRRRRRR *) -> "ERRORE IN STAMPA DI " ^ UriManager.string_of_uri uri
+ | e (* BRRRRRRRRR *) ->
+ Printf.sprintf "\nERRORE IN STAMPA DI %s\n%s\n"
+ (UriManager.string_of_uri uri) (Printexc.to_string e)
) sorted_uris_without_xpointer)
in
[],declarative,String.length parsed_text
| `CANCEL -> raise MatitaTypes.Cancel)
| _ -> ()
end;
+ ignore (buffer#move_mark (`NAME "beginning_of_statement")
+ ~where:((buffer#get_iter_at_mark (`NAME "locked"))#forward_chars
+ (Glib.Utf8.length skipped_txt))) ;
eval_with_engine
guistuff lexicon_status grafite_status user_goal skipped_txt nonskipped_txt
(TA.Executable (loc, ex))
(** text mark and tag representing locked part of a script *)
val locked_mark =
buffer#create_mark ~name:"locked" ~left_gravity:true buffer#start_iter
+ val beginning_of_statement_mark =
+ buffer#create_mark ~name:"beginning_of_statement"
+ ~left_gravity:true buffer#start_iter
val locked_tag = buffer#create_tag [`BACKGROUND "lightblue"; `EDITABLE false]
val error_tag = buffer#create_tag [`UNDERLINE `SINGLE; `FOREGROUND "red"]