src/Pure/General/position.ML
author wenzelm
Sun, 20 Jul 2008 23:06:55 +0200
changeset 27661 a5019f9ae068
parent 27426 c0ef698c0904
child 27736 3703dbd0cdea
permissions -rw-r--r--
added type range;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6118
caa439435666 fixed titles;
wenzelm
parents: 5010
diff changeset
     1
(*  Title:      Pure/General/position.ML
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
     4
23673
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
     5
Source positions.
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
     6
*)
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
     7
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
     8
signature POSITION =
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
     9
sig
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    10
  type T
27661
a5019f9ae068 added type range;
wenzelm
parents: 27426
diff changeset
    11
  type range = T * T
23673
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
    12
  val line_of: T -> int option
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    13
  val column_of: T -> int option
23673
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
    14
  val file_of: T -> string option
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    15
  val none: T
26882
9e824d8f4512 renamed Position.path to Path.position;
wenzelm
parents: 26633
diff changeset
    16
  val line_file: int -> string -> T
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    17
  val line: int -> T
23673
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
    18
  val file: string -> T
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    19
  val advance: Symbol.symbol -> T -> T
27426
c0ef698c0904 added get_id/put_id;
wenzelm
parents: 26890
diff changeset
    20
  val get_id: T -> string option
c0ef698c0904 added get_id/put_id;
wenzelm
parents: 26890
diff changeset
    21
  val put_id: string -> T -> T
25817
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
    22
  val of_properties: Markup.property list -> T
23627
f543538866a2 added property conversions;
wenzelm
parents: 22158
diff changeset
    23
  val properties_of: T -> Markup.property list
26052
7d5b3e34a735 added default_properties;
wenzelm
parents: 26003
diff changeset
    24
  val default_properties: T -> Markup.property list -> Markup.property list
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    25
  val str_of: T -> string
25817
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
    26
  val thread_data: unit -> T
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
    27
  val setmp_thread_data: T -> ('a -> 'b) -> 'a -> 'b
25954
682e84b60e5c added setmp_thread_data_seq;
wenzelm
parents: 25817
diff changeset
    28
  val setmp_thread_data_seq: T -> ('a -> 'b Seq.seq) -> 'a -> 'b Seq.seq
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    29
end;
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    30
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    31
structure Position: POSITION =
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    32
struct
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    33
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    34
(* datatype position *)
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    35
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    36
datatype T = Pos of (int * int) option * Markup.property list;
27661
a5019f9ae068 added type range;
wenzelm
parents: 27426
diff changeset
    37
type range = T * T
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    38
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    39
fun line_of (Pos (SOME (m, _), _)) = SOME m
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    40
  | line_of _ = NONE;
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    41
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    42
fun column_of (Pos (SOME (_, n), _)) = SOME n
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    43
  | column_of _ = NONE;
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    44
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    45
fun file_of (Pos (_, props)) = AList.lookup (op =) props Markup.fileN;
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    46
26882
9e824d8f4512 renamed Position.path to Path.position;
wenzelm
parents: 26633
diff changeset
    47
25817
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
    48
val none = Pos (NONE, []);
26882
9e824d8f4512 renamed Position.path to Path.position;
wenzelm
parents: 26633
diff changeset
    49
9e824d8f4512 renamed Position.path to Path.position;
wenzelm
parents: 26633
diff changeset
    50
fun line_file m name = Pos (SOME (m, 1), if name = "" then [] else [(Markup.fileN, name)]);
9e824d8f4512 renamed Position.path to Path.position;
wenzelm
parents: 26633
diff changeset
    51
fun line m = line_file m "";
9e824d8f4512 renamed Position.path to Path.position;
wenzelm
parents: 26633
diff changeset
    52
val file = line_file 1;
9e824d8f4512 renamed Position.path to Path.position;
wenzelm
parents: 26633
diff changeset
    53
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    54
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    55
fun advance "\n" (Pos (SOME (m, _), props)) = Pos (SOME (m + 1, 1), props)
26633
ff317b19e24e advance: do not count utf8 trailer bytes (which happen to be undefined or punctuation in iso-latin);
wenzelm
parents: 26052
diff changeset
    56
  | advance s (pos as Pos (SOME (m, n), props)) =
ff317b19e24e advance: do not count utf8 trailer bytes (which happen to be undefined or punctuation in iso-latin);
wenzelm
parents: 26052
diff changeset
    57
      if Symbol.is_regular s andalso not (Symbol.is_utf8_trailer s)
ff317b19e24e advance: do not count utf8 trailer bytes (which happen to be undefined or punctuation in iso-latin);
wenzelm
parents: 26052
diff changeset
    58
      then Pos (SOME (m, n + 1), props) else pos
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    59
  | advance _ pos = pos;
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    60
23627
f543538866a2 added property conversions;
wenzelm
parents: 22158
diff changeset
    61
f543538866a2 added property conversions;
wenzelm
parents: 22158
diff changeset
    62
(* markup properties *)
22158
ff4fc4ee9eb0 Add line_of, name_of destructors.
aspinall
parents: 15531
diff changeset
    63
27426
c0ef698c0904 added get_id/put_id;
wenzelm
parents: 26890
diff changeset
    64
fun get_id (Pos (_, props)) = AList.lookup (op =) props Markup.idN;
c0ef698c0904 added get_id/put_id;
wenzelm
parents: 26890
diff changeset
    65
fun put_id id (Pos (count, props)) = Pos (count, AList.update (op =) (Markup.idN, id) props);
c0ef698c0904 added get_id/put_id;
wenzelm
parents: 26890
diff changeset
    66
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    67
fun get_int props (name: string) =
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    68
  (case AList.lookup (op =) props name of
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    69
    NONE => NONE
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    70
  | SOME s => Int.fromString s);
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    71
25817
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
    72
fun of_properties props =
23627
f543538866a2 added property conversions;
wenzelm
parents: 22158
diff changeset
    73
  let
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    74
    val count =
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    75
      (case get_int props Markup.lineN of
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    76
        NONE => NONE
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    77
      | SOME m => SOME (m, the_default 1 (get_int props Markup.columnN)));
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    78
    fun property name = the_list (find_first (fn (x: string, _) => x = name) props);
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    79
  in (Pos (count, property Markup.fileN @ property Markup.idN)) end;
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    80
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    81
fun properties_of (Pos (count, props)) =
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    82
  (case count of
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    83
    NONE => []
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    84
  | SOME (m, n) => [(Markup.lineN, string_of_int m), (Markup.columnN, string_of_int n)]) @ props;
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    85
26052
7d5b3e34a735 added default_properties;
wenzelm
parents: 26003
diff changeset
    86
fun default_properties default props =
7d5b3e34a735 added default_properties;
wenzelm
parents: 26003
diff changeset
    87
  if exists (member (op =) Markup.position_properties o #1) props then props
7d5b3e34a735 added default_properties;
wenzelm
parents: 26003
diff changeset
    88
  else properties_of default @ props;
7d5b3e34a735 added default_properties;
wenzelm
parents: 26003
diff changeset
    89
25817
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
    90
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    91
(* str_of *)
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    92
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    93
fun str_of pos =
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    94
  let
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    95
    val props = properties_of pos;
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    96
    val s =
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    97
      (case (line_of pos, file_of pos) of
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    98
        (SOME m, NONE) => "(line " ^ string_of_int m ^ ")"
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    99
      | (SOME m, SOME name) => "(line " ^ string_of_int m ^ " of " ^ quote name ^ ")"
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   100
      | _ => "");
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   101
  in
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   102
    if null props then ""
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   103
    else (if s = "" then "" else " ") ^ Markup.markup (Markup.properties props Markup.position) s
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   104
  end;
25817
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
   105
23627
f543538866a2 added property conversions;
wenzelm
parents: 22158
diff changeset
   106
25817
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
   107
(* thread data *)
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
   108
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
   109
local val tag = Universal.tag () : T Universal.tag in
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
   110
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
   111
fun thread_data () = the_default none (Multithreading.get_data tag);
26890
f9ec18f7c0f6 setmp_thread_data: do nothing if Output.debugging;
wenzelm
parents: 26882
diff changeset
   112
f9ec18f7c0f6 setmp_thread_data: do nothing if Output.debugging;
wenzelm
parents: 26882
diff changeset
   113
fun setmp_thread_data pos f x =
f9ec18f7c0f6 setmp_thread_data: do nothing if Output.debugging;
wenzelm
parents: 26882
diff changeset
   114
  if ! Output.debugging then f x
f9ec18f7c0f6 setmp_thread_data: do nothing if Output.debugging;
wenzelm
parents: 26882
diff changeset
   115
  else Library.setmp_thread_data tag (thread_data ()) pos f x;
25817
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
   116
25954
682e84b60e5c added setmp_thread_data_seq;
wenzelm
parents: 25817
diff changeset
   117
fun setmp_thread_data_seq pos f seq =
682e84b60e5c added setmp_thread_data_seq;
wenzelm
parents: 25817
diff changeset
   118
  setmp_thread_data pos f seq |> Seq.wrap (fn pull => setmp_thread_data pos pull ());
682e84b60e5c added setmp_thread_data_seq;
wenzelm
parents: 25817
diff changeset
   119
25817
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
   120
end;
23673
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
   121
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
   122
end;