type options = option_value StringMap.t
let no_options = StringMap.empty
+type ast_command = (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command
+
type status = {
- aliases: DisambiguateTypes.environment; (** disambiguation aliases *)
+ aliases: DisambiguateTypes.environment;
+ multi_aliases: DisambiguateTypes.multiple_environment;
+ moo_content_rev: ast_command list;
proof_status: proof_status;
options: options;
objects: (UriManager.uri * string) list;
- (** in-scope objects, with their paths *)
+ notation_ids: CicNotation.notation_id list;
}
+let set_metasenv metasenv status =
+ let proof_status =
+ match status.proof_status with
+ | No_proof -> Intermediate metasenv
+ | Incomplete_proof ((uri, _, proof, ty), goal) ->
+ Incomplete_proof ((uri, metasenv, proof, ty), goal)
+ | Intermediate _ -> Intermediate metasenv
+ | Proof _ -> assert false
+ in
+ { status with proof_status = proof_status }
+
+let add_moo_content cmds status =
+ let content = status.moo_content_rev in
+ let content' =
+ List.fold_right
+ (fun cmd acc ->
+(* prerr_endline ("adding to moo command: " ^ GrafiteAstPp.pp_command cmd); *)
+ match cmd with
+ | GrafiteAst.Interpretation _
+ | GrafiteAst.Default _ ->
+ if List.mem cmd content then acc
+ else cmd :: acc
+ | GrafiteAst.Alias _ -> (* move Alias as the last inserted one *)
+ cmd :: (List.filter ((<>) cmd) acc)
+ | _ -> cmd :: acc)
+ cmds content
+ in
+(* prerr_endline ("new moo content: " ^ String.concat " " (List.map
+ GrafiteAstPp.pp_command content')); *)
+ { status with moo_content_rev = content' }
+
let dump_status status =
MatitaLog.message "status.aliases:\n";
MatitaLog.message
- (CicTextualParser2.EnvironmentP3.to_string status.aliases ^ "\n");
+ (DisambiguatePp.pp_environment status.aliases ^ "\n");
MatitaLog.message "status.proof_status:";
MatitaLog.message
(match status.proof_status with