| Cic.Const _ as t ->
PT.Ident (pp_t c t, None)
| Cic.Appl l -> PT.Appl (List.map (aux c) l)
| Cic.Const _ as t ->
PT.Ident (pp_t c t, None)
| Cic.Appl l -> PT.Appl (List.map (aux c) l)
| Cic.Lambda (Cic.Name n, s, t) ->
PT.Binder (`Lambda, (PT.Ident (n,None), Some (aux c s)),
aux (Some (Cic.Name n, Cic.Decl s)::c) t)
| Cic.Lambda (Cic.Name n, s, t) ->
PT.Binder (`Lambda, (PT.Ident (n,None), Some (aux c s)),
aux (Some (Cic.Name n, Cic.Decl s)::c) t)
| Cic.LetIn (Cic.Name n, s, ty, t) ->
PT.Binder (`Lambda, (PT.Ident (n,None), Some (aux c s)),
aux (Some (Cic.Name n, Cic.Def (s,ty))::c) t)
| Cic.LetIn (Cic.Name n, s, ty, t) ->
PT.Binder (`Lambda, (PT.Ident (n,None), Some (aux c s)),
aux (Some (Cic.Name n, Cic.Def (s,ty))::c) t)
| Cic.Sort (Cic.Type u) -> PT.Sort (`Type u)
| Cic.Sort Cic.Set -> PT.Sort `Set
| Cic.Sort (Cic.CProp u) -> PT.Sort (`CProp u)
| Cic.Sort (Cic.Type u) -> PT.Sort (`Type u)
| Cic.Sort Cic.Set -> PT.Sort `Set
| Cic.Sort (Cic.CProp u) -> PT.Sort (`CProp u)
(* no idea why ocaml wants this *)
let parsed_text_length = String.length parsed_text in
let dbd = LibraryDb.instance () in
(* no idea why ocaml wants this *)
let parsed_text_length = String.length parsed_text in
let dbd = LibraryDb.instance () in
try
ignore (buffer#move_mark (`NAME "beginning_of_statement")
~where:((buffer#get_iter_at_mark (`NAME "locked"))#forward_chars
try
ignore (buffer#move_mark (`NAME "beginning_of_statement")
~where:((buffer#get_iter_at_mark (`NAME "locked"))#forward_chars
and eval_statement include_paths (buffer : GText.buffer) guistuff
grafite_status user_goal script statement
=
and eval_statement include_paths (buffer : GText.buffer) guistuff
grafite_status user_goal script statement
=
match statement with
| `Raw text ->
if Pcre.pmatch ~rex:only_dust_RE text then raise Margin;
let ast =
wrap_with_make include_paths
(GrafiteParser.parse_statement (Ulexing.from_utf8_string text))
match statement with
| `Raw text ->
if Pcre.pmatch ~rex:only_dust_RE text then raise Margin;
let ast =
wrap_with_make include_paths
(GrafiteParser.parse_statement (Ulexing.from_utf8_string text))
- | `Ast (st, text) -> (GrafiteTypes.get_estatus grafite_status, st), text
+ | `Ast (st, text) -> (grafite_status, st), text
let text_of_loc floc =
let nonskipped_txt,_ = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in
let start, stop = HExtlib.loc_of_floc floc in
let text_of_loc floc =
let nonskipped_txt,_ = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in
let start, stop = HExtlib.loc_of_floc floc in
- LexiconSync.time_travel
- ~present:(GrafiteTypes.get_estatus cur_grafite_status)
- ~past:(GrafiteTypes.get_estatus grafite_status);
+ LexiconSync.time_travel ~present:cur_grafite_status ~past:grafite_status;
GrafiteSync.time_travel ~present:cur_grafite_status ~past:grafite_status;
statements <- new_statements;
history <- new_history;
GrafiteSync.time_travel ~present:cur_grafite_status ~past:grafite_status;
statements <- new_statements;
history <- new_history;
(* FIXME: this is not correct since there is no undo for
* library_objects.set_default... *)
GrafiteSync.time_travel ~present:self#grafite_status ~past:grafite_status;
(* FIXME: this is not correct since there is no undo for
* library_objects.set_default... *)
GrafiteSync.time_travel ~present:self#grafite_status ~past:grafite_status;
- LexiconSync.time_travel
- ~present:(GrafiteTypes.get_estatus self#grafite_status)
- ~past:(GrafiteTypes.get_estatus grafite_status)
+ LexiconSync.time_travel ~present:self#grafite_status ~past:grafite_status