A flag DEFS_CHAIN_HISTORY can be used to improve the error message
authorobua
Tue Jun 07 20:04:41 2005 +0200 (2005-06-07)
changeset 1631379b37d5e50b1
parent 16312 d13addf9101e
child 16314 7102a1aaecfd
A flag DEFS_CHAIN_HISTORY can be used to improve the error message
in case a cycle has been detected. If it is switched off and a cycle has been
detected, the user is notified that there is such a flag.
src/Pure/theory.ML
     1.1 --- a/src/Pure/theory.ML	Tue Jun 07 17:13:58 2005 +0200
     1.2 +++ b/src/Pure/theory.ML	Tue Jun 07 20:04:41 2005 +0200
     1.3 @@ -393,12 +393,16 @@
     1.4     | prts => Pretty.block (pretty_const pp (c, T) @
     1.5        [Pretty.brk 1, Pretty.str ("depends via " ^ quote def ^ " on")]) :: prts) path [];
     1.6  
     1.7 +fun chain_history_msg s = 
     1.8 +    if Defs.chain_history () then s^": " 
     1.9 +    else s^" (set DEFS_CHAIN_HISTORY=ON for full history): "
    1.10 +
    1.11  fun defs_circular pp path =
    1.12 -  Pretty.str "Cyclic dependency in definitions: " :: pretty_path pp path
    1.13 +  Pretty.str (chain_history_msg "Cyclic dependency of definitions") :: pretty_path pp path
    1.14    |> Pretty.chunks |> Pretty.string_of;
    1.15  
    1.16  fun defs_infinite_chain pp path =
    1.17 -  Pretty.str "Infinite chain in definitions: " :: pretty_path pp path
    1.18 +  Pretty.str (chain_history_msg "Infinite chain of definitions") :: pretty_path pp path
    1.19    |> Pretty.chunks |> Pretty.string_of;
    1.20  
    1.21  fun defs_clash def1 def2 = "Type clash in definitions " ^ quote def1 ^ " and " ^ quote def2;