File ‹Feedback.ML›
structure C_Files = Theory_Data
(struct
type T = {main: string,
files: (Token.file * Position.T ) Symtab.table Symtab.table}
val empty = {main = "", files = Symtab.empty}
val merge = Utils.fast_merge (fn ({files=files1,...}, {files=files2,...}) =>
{main = "", files = Symtab.join (fn _ => Symtab.merge (K false)) (files1, files2)})
end);
structure C_Files =
struct
open C_Files
val get_main = #main o get
val get_files = #files o get
fun map_main' f {main, files} = {main = f main, files = files}
fun map_files' f {main, files} = {main = main, files = f files}
val map_main = map o map_main'
val map_files = map o map_files'
fun get_current_files thy =
let
val {main, files} = get thy
in the_default Symtab.empty (Symtab.lookup files main) end
val default_file = ({src_path = Path.root, lines = [], digest=SHA1.fake "", pos = Position.none}, Position.none)
fun get_file thy main name = Symtab.lookup (#files (get thy)) main
|> Option.mapPartial (fn tab => Symtab.lookup tab name)
fun map_file main name f =
map (map_files'
(Symtab.map_default (main, Symtab.empty) (Symtab.map_default (name, default_file) f)))
fun get_current_file thy = get_file thy (get_main thy)
fun map_current_file name f thy = map_file (get_main thy) name f thy
end
signature FEEDBACK =
sig
exception WantToExit of string
val level : int Config.T
val verbose : bool Config.T
val get_num_errors_val : Proof.context -> int
val reset_num_errors : Proof.context -> Proof.context
val get_threshold : Proof.context -> int option
val map_threshold : (int option -> int option) -> Proof.context -> Proof.context
val transfer_error_state : Proof.context -> Proof.context -> Proof.context
val errorStr : Proof.context -> Region.t * string -> unit
val errorStr' : Proof.context -> SourcePos.t * SourcePos.t * string -> unit
val warnStr' : Proof.context -> SourcePos.t * SourcePos.t * string -> unit
val informStr : Proof.context -> int * string -> unit
val informStr' : Proof.context -> int * SourcePos.t * SourcePos.t * string -> unit
val error_region : Proof.context -> Region.t -> string -> 'a
val error_range : Proof.context -> SourcePos.t -> SourcePos.t -> string -> 'a
val error_pos : Proof.context -> SourcePos.t -> string -> 'a
val report_error : (string * Position.T option) -> unit
val report_warning : (string * Position.T option) -> unit
val report_inform : (string * Position.T option) -> unit
val errorf : ((string * Position.T option) -> unit) Unsynchronized.ref
val warnf : ((string * Position.T option) -> unit) Unsynchronized.ref
val informf : ((string * Position.T option) -> unit) Unsynchronized.ref
val timestamp : string -> string
val in_target : xstring -> (local_theory -> local_theory) -> local_theory -> local_theory
end
structure Feedback :> FEEDBACK =
struct
val level = Attrib.setup_config_int @{binding "c_parser_feedback_level"} (K 0)
val verbose = Attrib.setup_config_bool @{binding "c_parser_verbose"} (K false)
fun pos_of_cpos (file:Token.file) cpos = if SourcePos.is_bogus cpos then Position.none else
let
val c = SourcePos.column cpos
val l = SourcePos.line cpos
val {lines, pos,...} = file
val lines = take (l - 1) lines
val offset_lines = fold (fn l => fn off => off + (length (Symbol.explode l)) + 1) lines 1
val offset = offset_lines + c
val end_offset = 0
in
Position.make {line = l, offset = offset, end_offset= end_offset, props = #props (Position.dest pos)}
end
fun map_column f p = SourcePos.make {column = f (SourcePos.column p), file = SourcePos.file p, line = SourcePos.line p}
fun pos_of_crange file cpos1 cpos2 =
let
val pos1 = pos_of_cpos file cpos1
val pos2 = pos_of_cpos file (map_column (fn n => n + 1) cpos2)
in
Position.range_position (pos1, pos2)
end
fun pos_of_cregion (file: Token.file) region =
let
val fpos = #pos file
in
case Region.left region of
NONE => fpos
| SOME l => (case Region.right region of
NONE => pos_of_cpos file l
| SOME r => pos_of_crange file l r)
end
exception WantToExit of string
structure Data = Proof_Data(
struct
type T = int Synchronized.var * (int option)
val init = (fn _ => (Synchronized.var "num_errors" 0, NONE))
end
);
val get_num_errors = fst o Data.get
fun map_num_errors f = Data.map (apfst f)
fun transfer_error_state ctxt1 ctxt2 = Data.map (K (Data.get ctxt1)) ctxt2
val get_num_errors_val = Synchronized.value o get_num_errors
fun reset_num_errors ctxt = map_num_errors (K (Synchronized.var "num_errors" 0)) ctxt
fun incr_num_errors ctxt =
let
val v = get_num_errors ctxt
in Synchronized.guarded_access v (fn n => SOME (n, n + 1)) end
val get_threshold = snd o Data.get
fun map_threshold f = Data.map (apsnd f)
fun command_output output (s, NONE) = output s
| command_output output (s, SOME command_thread_pos) =
let
val current_thread_pos = Position.thread_data ()
val _ =
if command_thread_pos <> current_thread_pos then
Position.setmp_thread_data command_thread_pos output s
else ()
in
output s
end
val report_error = command_output Output.error_message
val report_warning = command_output warning
val report_inform = command_output tracing
val errorf = Unsynchronized.ref report_error
val warnf = Unsynchronized.ref report_warning
val informf = Unsynchronized.ref report_inform
val _ = Option.map
fun message ctxt markup r s =
let
val thy = Proof_Context.theory_of ctxt
val file = \<^try>‹Region.left r
|> Option.map (SourcePos.file #> Path.explode #> Path.base #> Path.file_name)
|> Option.mapPartial (C_Files.get_current_file thy)
catch _ => NONE›
in
case file of
NONE => (Region.toString r ^ ": " ^ s, NONE)
| SOME (f, command_thread_pos) =>
let
val pos = pos_of_cregion f r
val str = s ^ ": " ^ Position.here pos
in
(str, SOME command_thread_pos)
end
end
fun message' ctxt markup l r = message ctxt markup (Region.make {left = l, right = r})
fun message_pos ctxt markup p = message ctxt markup (Region.make {left = p, right = SourcePos.bogus})
fun informStr0 ctxt (v,s) = if v <= Config.get ctxt level then !informf s else ()
fun informStr' ctxt (v,l,r,s) =
informStr0 ctxt (v, message' ctxt Markup.tracing l r s)
fun informStr ctxt (v, s) = informStr0 ctxt (v, (s, NONE))
fun errorStr ctxt (r, s) =
let
val msg = message ctxt Markup.error r s
val _ = !errorf msg
val n = incr_num_errors ctxt
val threshold = get_threshold ctxt
in
if is_some threshold andalso n > the threshold then
raise WantToExit "Too many errors - aborted."
else ()
end
fun errorStr' ctxt (l,r,s) = errorStr ctxt (Region.make {left = l, right = r}, s)
fun warnStr' ctxt (l,r,s) =
!warnf ( message' ctxt Markup.warning l r s |> apfst (prefix "Warning "))
fun timestamp s = Time.fmt 0 (Time.now()) ^ ": " ^ s
fun raise_error (msg as (s, _)) =
(!errorf msg; error s)
fun error_region ctxt r s = raise_error (message ctxt Markup.error r s)
fun error_range ctxt l r s = raise_error (message' ctxt Markup.error l r s)
fun error_pos ctxt p s = raise_error (message_pos ctxt Markup.error p s)
fun in_target name f lthy =
let
val (reenter, target_lthy) = Target_Context.switch_named_cmd (SOME (name, Position.none)) (Context.Proof lthy)
in
target_lthy
|> transfer_error_state lthy
|> f
|> (fn lthy' =>
lthy'
|> reenter
|> Context.the_proof
|> transfer_error_state lthy')
end
end;
structure More_Local_Theory =
struct
open More_Local_Theory
fun in_theory f = gen_in_theory Feedback.transfer_error_state f
fun in_theory_result f = gen_in_theory_result Feedback.transfer_error_state f
end