- (** return a pair of "xml" (as defined in Xml module) representing the *
- * current proof type and body, respectively *)
- method toXml: Xml.token Stream.t * Xml.token Stream.t
- method toString: string
- end
+let set_option status name value =
+ let mangle_dir s =
+ let s = Str.global_replace (Str.regexp "//+") "/" s in
+ let s = Str.global_replace (Str.regexp "/$") "" s in
+ s
+ in
+ let types =
+ [ "baseuri", (`String, mangle_dir);
+ "basedir", (`String, mangle_dir);
+ ]
+ in
+ let ty_and_mangler =
+ try
+ List.assoc name types
+ with Not_found -> command_error (sprintf "Unknown option \"%s\"" name)
+ in
+ let value =
+ match ty_and_mangler with
+ | `String, f -> String (f value)
+ | `Int, f ->
+ (try
+ Int (int_of_string (f value))
+ with Failure _ ->
+ command_error (sprintf "Not an integer value \"%s\"" value))
+ in
+ if StringMap.mem name status.options && name = "baseuri" then
+ command_error "Redefinition of 'baseuri' is forbidden."
+ else
+ { status with options = StringMap.add name value status.options }
+
+let add_moo_content cmds status =
+ let content, metadata = 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', metadata }