prefer tight Markup.print_int/parse_int for property values;
authorwenzelm
Wed Nov 28 16:09:05 2012 +0100 (2012-11-28 ago)
changeset 50254935ac0ad7e83
parent 50253 41fd9f68614b
child 50255 d0ec1f0d1d7d
prefer tight Markup.print_int/parse_int for property values;
src/Pure/General/position.ML
src/Pure/System/isabelle_process.ML
     1.1 --- a/src/Pure/General/position.ML	Wed Nov 28 16:07:17 2012 +0100
     1.2 +++ b/src/Pure/General/position.ML	Wed Nov 28 16:09:05 2012 +0100
     1.3 @@ -131,14 +131,14 @@
     1.4      fun get name =
     1.5        (case Properties.get props name of
     1.6          NONE => 0
     1.7 -      | SOME s => the_default 0 (Int.fromString s));
     1.8 +      | SOME s => Markup.parse_int s);
     1.9    in
    1.10      make {line = get Markup.lineN, offset = get Markup.offsetN,
    1.11        end_offset = get Markup.end_offsetN, props = props}
    1.12    end;
    1.13  
    1.14  
    1.15 -fun value k i = if valid i then [(k, string_of_int i)] else [];
    1.16 +fun value k i = if valid i then [(k, Markup.print_int i)] else [];
    1.17  
    1.18  fun properties_of (Pos ((i, j, k), props)) =
    1.19    value Markup.lineN i @ value Markup.offsetN j @ value Markup.end_offsetN k @ props;
    1.20 @@ -146,8 +146,8 @@
    1.21  val def_properties_of = properties_of #> (map (fn (x, y) => ("def_" ^ x, y)));
    1.22  
    1.23  fun entity_properties_of def id pos =
    1.24 -  if def then (Markup.defN, string_of_int id) :: properties_of pos
    1.25 -  else (Markup.refN, string_of_int id) :: def_properties_of pos;
    1.26 +  if def then (Markup.defN, Markup.print_int id) :: properties_of pos
    1.27 +  else (Markup.refN, Markup.print_int id) :: def_properties_of pos;
    1.28  
    1.29  fun default_properties default props =
    1.30    if exists (member (op =) Markup.position_properties o #1) props then props
    1.31 @@ -186,8 +186,8 @@
    1.32      val props = properties_of pos;
    1.33      val s =
    1.34        (case (line_of pos, file_of pos) of
    1.35 -        (SOME i, NONE) => "(line " ^ string_of_int i ^ ")"
    1.36 -      | (SOME i, SOME name) => "(line " ^ string_of_int i ^ " of " ^ quote name ^ ")"
    1.37 +        (SOME i, NONE) => "(line " ^ Markup.print_int i ^ ")"
    1.38 +      | (SOME i, SOME name) => "(line " ^ Markup.print_int i ^ " of " ^ quote name ^ ")"
    1.39        | (NONE, SOME name) => "(file " ^ quote name ^ ")"
    1.40        | _ => "");
    1.41    in
     2.1 --- a/src/Pure/System/isabelle_process.ML	Wed Nov 28 16:07:17 2012 +0100
     2.2 +++ b/src/Pure/System/isabelle_process.ML	Wed Nov 28 16:09:05 2012 +0100
     2.3 @@ -99,7 +99,7 @@
     2.4    if body = "" then ()
     2.5    else
     2.6      message false mbox name
     2.7 -      ((case opt_serial of SOME i => cons (Markup.serialN, string_of_int i) | _ => I)
     2.8 +      ((case opt_serial of SOME i => cons (Markup.serialN, Markup.print_int i) | _ => I)
     2.9          (Position.properties_of (Position.thread_data ()))) body;
    2.10  
    2.11  fun message_output mbox channel =