String.sub s 0 nl_pos
with Not_found -> s
- (** creates a statement AST for the Goal tactic, e.g. "goal 7" *)
-let goal_ast n =
- let module A = GrafiteAst in
- let loc = HExtlib.dummy_floc in
- A.Executable (loc, A.Tactical (loc,
- A.Tactic (loc, A.Goal (loc, n)),
- Some (A.Dot loc)))
-
type guistuff = {
mathviewer:MatitaTypes.mathViewer;
urichooser: UriManager.uri list -> UriManager.uri list;
guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
[], "", parsed_text_length
| TA.WHint (loc, term) ->
- let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term),0) in
+ let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term, []),0) in
let l = List.map fst (MQ.experimental_hint ~dbd s) in
let entry = `Whelp (pp_macro mac, l) in
guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
| [uri] ->
let suri = UriManager.string_of_uri uri in
let ast loc =
- TA.Executable (loc, (TA.Tactical (loc,
- TA.Tactic (loc,
- TA.Apply (loc, CicNotationPt.Uri (suri, None))),
- Some (TA.Dot loc)))) in
+ TA.Executable (loc, (TA.Tactic (loc,
+ Some (TA.Apply (loc, CicNotationPt.Uri (suri, None))),
+ TA.Dot loc))) in
let text =
comment parsed_text ^ "\n" ^
pp_eager_statement_ast (ast HExtlib.dummy_floc) in
guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv));
[], "", parsed_text_length
| TA.Inline (_,style,suri,prefix) ->
- let dbd = LibraryDb.instance () in
- let uris =
- let sql_pat =
- (Pcre.replace ~rex:(Pcre.regexp "_") ~templ:"\\_" suri) ^ "%" in
- let query =
- sprintf ("SELECT source FROM %s WHERE source LIKE \"%s\" UNION "^^
- "SELECT source FROM %s WHERE source LIKE \"%s\"")
- (MetadataTypes.name_tbl ()) sql_pat
- MetadataTypes.library_name_tbl sql_pat in
- let result = HMysql.exec dbd query in
- HMysql.map result
- (function cols ->
- match cols.(0) with
- Some s -> UriManager.uri_of_string s
- | _ -> assert false)
- in
-prerr_endline "Inizio sorting";
- let sorted_uris = MetadataDeps.topological_sort ~dbd uris in
-prerr_endline "Fine sorting";
- let sorted_uris_without_xpointer =
- HExtlib.filter_map
- (function uri ->
- let s =
- Pcre.replace ~rex:(Pcre.regexp "#xpointer\\(1/1\\)") ~templ:""
- (UriManager.string_of_uri uri) in
- try
- ignore (Pcre.exec ~rex:(Pcre.regexp"#xpointer") s);
- None
- with
- Not_found ->
- Some (UriManager.uri_of_string s)
- ) sorted_uris
- in
- let declarative =
- String.concat "\n\n"
- (List.map
- (fun uri ->
-prerr_endline ("Stampo " ^ UriManager.string_of_uri uri);
- try
- ObjPp.obj_to_string 78 style prefix (* FG: mi pare meglio 78 *)
- (fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri))
- with
- | 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
+ let str = ApplyTransformation.txt_of_inline_macro style suri prefix in
+ [], str, String.length parsed_text
and eval_executable include_paths (buffer : GText.buffer) guistuff
lexicon_status grafite_status user_goal unparsed_text skipped_txt nonskipped_txt
with
| Margin -> self#notify
| Not_found -> assert false
+ | Invalid_argument "Array.make" -> HLog.error "The script is too big!\n"
| exc -> self#notify; raise exc
method retract () =
self#notify
with
| Margin -> self#notify
+ | Invalid_argument "Array.make" -> HLog.error "The script is too big!\n"
| exc -> self#notify; raise exc
method private getFuture =
set_star (Filename.basename self#ppFilename) false
method goto (pos: [`Top | `Bottom | `Cursor]) () =
+ try
let old_locked_mark =
`MARK
(buffer#create_mark ~name:"old_locked_mark"
| Margin -> dispose_remember (); dispose_old_locked_mark (); self#notify
| exc -> dispose_remember (); dispose_old_locked_mark ();
self#notify; raise exc)
-
+ with Invalid_argument "Array.make" ->
+ HLog.error "The script is too big!\n"
+
method onGoingProof () =
match self#grafite_status.proof_status with
| No_proof | Proof _ -> false
| HExtlib.Localized _
| CicNotationParser.Parse_error _ -> false
| Margin | End_of_file -> true
+ | Invalid_argument "Array.make" -> false
(* debug *)
method dump () =