+let rec get_ast status ~compiling ~asserted ~include_paths strm =
+ match GrafiteParser.parse_statement status strm with
+ (GrafiteAst.Executable
+ (_,GrafiteAst.NCommand (_,GrafiteAst.Include (_,_,mafilename)))) as cmd
+ ->
+ let already_included = NCicLibrary.get_transitively_included status in
+ let asserted,_ =
+ assert_ng ~already_included ~compiling ~asserted ~include_paths
+ mafilename
+ in
+ asserted,cmd
+ | cmd -> asserted,cmd
+
+and eval_from_stream ~compiling ~asserted ~include_paths ?do_heavy_checks status str cb =
+ let matita_debug = Helm_registry.get_bool "matita.debug" in
+ let rec loop asserted status str =
+ let asserted,stop,status,str =
+ try
+ let cont =
+ try Some (get_ast status ~compiling ~asserted ~include_paths str)
+ with End_of_file -> None in
+ match cont with
+ | None -> asserted, true, status, str
+ | Some (asserted,ast) ->
+ cb status ast;
+ let new_statuses =
+ eval_ast ~include_paths ?do_heavy_checks status ("",0,ast) in
+ let status =
+ match new_statuses with
+ [s,None] -> s
+ | _::(_,Some (_,value))::_ ->
+ raise (TryingToAdd (lazy (GrafiteAstPp.pp_alias value)))
+ | _ -> assert false in
+ (* CSC: complex patch to re-build the lexer since the tokens may
+ have changed. Note: this way we loose look-ahead tokens.
+ Hence the "include" command must be terminated (no look-ahead) *)
+ let str =
+ match ast with
+ (GrafiteAst.Executable
+ (_,GrafiteAst.NCommand
+ (_,(GrafiteAst.Include _ | GrafiteAst.Notation _)))) ->
+ GrafiteParser.parsable_statement status
+ (GrafiteParser.strm_of_parsable str)
+ | _ -> str
+ in
+ asserted, false, status, str
+ with exn when not matita_debug ->
+ raise (EnrichedWithStatus (exn, status))
+ in
+ if stop then asserted,status else loop asserted status str
+ in
+ loop asserted status str
+
+and compile ~compiling ~asserted ~include_paths fname =
+ if List.mem fname compiling then raise (CircularDependency fname);
+ let compiling = fname::compiling in