- let baseuri = GrafiteTypes.get_string_option new_status "baseuri" in
- List.fold_left (
- fun (initial_space,status,acc) (k,((v,_) as value)) ->
- let b =
- try
- UM.buri_of_uri (UM.uri_of_string v) = baseuri
- with
- UriManager.IllFormedUri _ -> false (* v is a description, not a URI *)
- in
- if b then
- initial_space,status,acc
- else
- let new_text =
- let initial_space =
- if initial_space = "" then "\n" else initial_space in
- initial_space ^
- DisambiguatePp.pp_environment
- (DisambiguateTypes.Environment.add k value
- DisambiguateTypes.Environment.empty) in
- let new_status =
- MatitaSync.set_proof_aliases status [k,value]
- in
- "\n",new_status,((new_status, (new_text, dummy_st))::acc)
- ) (initial_space,status,[]) new_aliases in
- let parsed_text = initial_space ^ parsed_text in
- let res =
- List.rev new_status_and_text_list_rev @ new_status_and_text_list' @
- [new_status, (parsed_text, st)]
+ List.fold_right (
+ fun (_,alias) (initial_space,acc) ->
+ match alias with
+ None -> initial_space,initial_space::acc
+ | Some (k,((v,_) as value)) ->
+ let new_text =
+ let initial_space =
+ if initial_space = "" then "\n" else initial_space
+ in
+ initial_space ^
+ DisambiguatePp.pp_environment
+ (DisambiguateTypes.Environment.add k value
+ DisambiguateTypes.Environment.empty)
+ in
+ "\n",new_text::acc
+ ) enriched_history_fragment (initial_space,[]) in
+ let new_text_list_rev =
+ match enriched_history_fragment,new_text_list_rev with
+ (_,None)::_, initial_space::tl -> (initial_space ^ parsed_text)::tl
+ | _,_ -> assert false