Binding.str_of: removed verbose feature, include qualifier in output;
authorwenzelm
Sat Mar 07 11:32:31 2009 +0100 (2009-03-07)
changeset 30335b3ef64cadcad
parent 30334 a2f236a717fa
child 30336 efd1bec4630a
Binding.str_of: removed verbose feature, include qualifier in output;
renamed Binding.add_prefix to Binding.prefix;
src/Pure/General/binding.ML
src/Pure/Isar/class.ML
src/Pure/Isar/expression.ML
     1.1 --- a/src/Pure/General/binding.ML	Sat Mar 07 11:31:41 2009 +0100
     1.2 +++ b/src/Pure/General/binding.ML	Sat Mar 07 11:32:31 2009 +0100
     1.3 @@ -11,7 +11,6 @@
     1.4  sig
     1.5    type binding
     1.6    val dest: binding -> (string * bool) list * bstring
     1.7 -  val verbose: bool ref
     1.8    val str_of: binding -> string
     1.9    val make: bstring * Position.T -> binding
    1.10    val pos_of: binding -> Position.T
    1.11 @@ -23,7 +22,7 @@
    1.12    val qualify: bool -> string -> binding -> binding
    1.13    val prefix_of: binding -> (string * bool) list
    1.14    val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
    1.15 -  val add_prefix: bool -> string -> binding -> binding
    1.16 +  val prefix: bool -> string -> binding -> binding
    1.17  end;
    1.18  
    1.19  structure Binding: BINDING =
    1.20 @@ -47,20 +46,9 @@
    1.21  
    1.22  fun dest (Binding {prefix, qualifier, name, ...}) = (prefix @ qualifier, name);
    1.23  
    1.24 -
    1.25 -(* diagnostic output *)
    1.26 -
    1.27 -val verbose = ref false;
    1.28 -
    1.29 -val str_of_components = implode o map (fn (s, true) => s ^ "!" | (s, false) => s ^ "?");
    1.30 -
    1.31  fun str_of (Binding {prefix, qualifier, name, pos}) =
    1.32    let
    1.33 -    val text =
    1.34 -      if ! verbose then
    1.35 -        (if null prefix then "" else enclose "(" ")" (str_of_components prefix)) ^
    1.36 -          str_of_components qualifier ^ name
    1.37 -      else name;
    1.38 +    val text = space_implode "." (map #1 qualifier @ [name]);
    1.39      val props = Position.properties_of pos;
    1.40    in Markup.markup (Markup.properties props (Markup.binding name)) text end;
    1.41  
    1.42 @@ -85,8 +73,8 @@
    1.43  (* user qualifier *)
    1.44  
    1.45  fun qualify _ "" = I
    1.46 -  | qualify mandatory qual = map_binding (fn (prefix, qualifier, name, pos) =>
    1.47 -      (prefix, (qual, mandatory) :: qualifier, name, pos));
    1.48 +  | qualify strict qual = map_binding (fn (prefix, qualifier, name, pos) =>
    1.49 +      (prefix, (qual, strict) :: qualifier, name, pos));
    1.50  
    1.51  
    1.52  (* system prefix *)
    1.53 @@ -96,8 +84,8 @@
    1.54  fun map_prefix f = map_binding (fn (prefix, qualifier, name, pos) =>
    1.55    (f prefix, qualifier, name, pos));
    1.56  
    1.57 -fun add_prefix _ "" = I
    1.58 -  | add_prefix mandatory prfx = map_prefix (cons (prfx, mandatory));
    1.59 +fun prefix _ "" = I
    1.60 +  | prefix strict prfx = map_prefix (cons (prfx, strict));
    1.61  
    1.62  end;
    1.63  
     2.1 --- a/src/Pure/Isar/class.ML	Sat Mar 07 11:31:41 2009 +0100
     2.2 +++ b/src/Pure/Isar/class.ML	Sat Mar 07 11:32:31 2009 +0100
     2.3 @@ -66,8 +66,7 @@
     2.4  
     2.5      (* canonical interpretation *)
     2.6      val base_morph = inst_morph
     2.7 -      $> Morphism.binding_morphism
     2.8 -           (Binding.add_prefix false (class_prefix class))
     2.9 +      $> Morphism.binding_morphism (Binding.prefix false (class_prefix class))
    2.10        $> Element.satisfy_morphism (the_list wit);
    2.11      val defs = these_defs thy sups;
    2.12      val eq_morph = Element.eq_morphism thy defs;
     3.1 --- a/src/Pure/Isar/expression.ML	Sat Mar 07 11:31:41 2009 +0100
     3.2 +++ b/src/Pure/Isar/expression.ML	Sat Mar 07 11:32:31 2009 +0100
     3.3 @@ -186,7 +186,7 @@
     3.4      val inst = Symtab.make insts'';
     3.5    in
     3.6      (Element.inst_morphism (ProofContext.theory_of ctxt) (instT, inst) $>
     3.7 -      Morphism.binding_morphism (Binding.add_prefix strict prfx), ctxt')
     3.8 +      Morphism.binding_morphism (Binding.prefix strict prfx), ctxt')
     3.9    end;
    3.10  
    3.11