-
-let filename () =
- try
- Helm_registry.get "matita.filename"
- with Helm_registry.Key_not_found "matita.filename" ->
- try
- match Helm_registry.get_list Helm_registry.string "matita.args" with
- | [x] ->
- HLog.warn ("Using matita.args as filename: "^x);
- Helm_registry.set "matita.filename" x;
- x
- | _ -> raise (Failure "no (or more than one) filename to compile")
- with Helm_registry.Key_not_found "matita.filename" ->
- raise (Failure "Unable to get current file name")
-;;