* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
open GrafiteTypes
"matita.includes"))
with
| GrafiteEngine.Drop -> pp_ocaml_mode ()
+ | GrafiteEngine.Macro (floc,_) ->
+ let x, y = HExtlib.loc_of_floc floc in
+ HLog.error
+ (sprintf "A macro has been found in a script at %d-%d" x y);
+ interactive_loop ()
| Sys.Break -> HLog.error "user break!"; interactive_loop ()
| GrafiteTypes.Command_error _ -> interactive_loop ()
| End_of_file ->
print_newline ();
clean_exit (Some 0)
| HExtlib.Localized (floc,CicNotationParser.Parse_error err) ->
- let (x, y) = HExtlib.loc_of_floc floc in
- HLog.error (sprintf "Parse error at %d-%d: %s" x y err);
- interactive_loop ()
+ let x, y = HExtlib.loc_of_floc floc in
+ HLog.error (sprintf "Parse error at %d-%d: %s" x y err);
+ interactive_loop ()
| exn -> HLog.error (Printexc.to_string exn); interactive_loop ()
let go () =
MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
LibraryDb.create_owner_environment ();
CicEnvironment.set_trust (* environment trust *)
- (let trust = Helm_registry.get_bool "matita.environment_trust" in
+ (let trust =
+ Helm_registry.get_opt_default Helm_registry.get_bool
+ ~default:true "matita.environment_trust" in
fun _ -> trust);
let include_paths =
Helm_registry.get_list Helm_registry.string "matita.includes" in
clean_exit (Some 1)
else
pp_ocaml_mode ()
+ | GrafiteEngine.Macro (floc,_) ->
+ let x, y = HExtlib.loc_of_floc floc in
+ HLog.error
+ (sprintf "A macro has been found in a script at %d-%d" x y);
+ if mode = `COMPILER then
+ clean_exit (Some 1)
+ else
+ pp_ocaml_mode ()
| HExtlib.Localized (floc,CicNotationParser.Parse_error err) ->
let (x, y) = HExtlib.loc_of_floc floc in
HLog.error (sprintf "Parse error at %d-%d: %s" x y err);