src/Pure/General/position.ML
author wenzelm
Sat, 12 Apr 2008 17:00:47 +0200
changeset 26633 ff317b19e24e
parent 26052 7d5b3e34a735
child 26882 9e824d8f4512
permissions -rw-r--r--
advance: do not count utf8 trailer bytes (which happen to be undefined or punctuation in iso-latin);
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
23673
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
    11
  val line_of: T -> int option
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    12
  val column_of: T -> int option
23673
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
    13
  val file_of: T -> string option
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    14
  val none: T
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    15
  val line: int -> T
23673
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
    16
  val file: string -> T
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
    17
  val path: Path.T -> T
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    18
  val advance: Symbol.symbol -> T -> T
25817
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
    19
  val of_properties: Markup.property list -> T
23627
f543538866a2 added property conversions;
wenzelm
parents: 22158
diff changeset
    20
  val properties_of: T -> Markup.property list
26052
7d5b3e34a735 added default_properties;
wenzelm
parents: 26003
diff changeset
    21
  val default_properties: T -> Markup.property list -> Markup.property list
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    22
  val str_of: T -> string
25817
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
    23
  val thread_data: unit -> T
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
    24
  val setmp_thread_data: T -> ('a -> 'b) -> 'a -> 'b
25954
682e84b60e5c added setmp_thread_data_seq;
wenzelm
parents: 25817
diff changeset
    25
  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
    26
end;
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    27
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    28
structure Position: POSITION =
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    29
struct
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
(* datatype position *)
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    32
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    33
datatype T = Pos of (int * int) option * Markup.property list;
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    34
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    35
fun line_of (Pos (SOME (m, _), _)) = SOME m
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    36
  | line_of _ = NONE;
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    37
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    38
fun column_of (Pos (SOME (_, n), _)) = SOME n
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    39
  | column_of _ = NONE;
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    40
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    41
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
    42
25817
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
    43
val none = Pos (NONE, []);
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    44
fun line m = Pos (SOME (m, 1), []);
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    45
fun file name = Pos (SOME (1, 1), [(Markup.fileN, name)]);
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    46
val path = file o Path.implode o Path.expand;
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    47
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    48
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
    49
  | 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
    50
      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
    51
      then Pos (SOME (m, n + 1), props) else pos
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    52
  | advance _ pos = pos;
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    53
23627
f543538866a2 added property conversions;
wenzelm
parents: 22158
diff changeset
    54
f543538866a2 added property conversions;
wenzelm
parents: 22158
diff changeset
    55
(* markup properties *)
22158
ff4fc4ee9eb0 Add line_of, name_of destructors.
aspinall
parents: 15531
diff changeset
    56
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    57
fun get_int props (name: string) =
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    58
  (case AList.lookup (op =) props name of
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    59
    NONE => NONE
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    60
  | SOME s => Int.fromString s);
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    61
25817
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
    62
fun of_properties props =
23627
f543538866a2 added property conversions;
wenzelm
parents: 22158
diff changeset
    63
  let
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    64
    val count =
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    65
      (case get_int props Markup.lineN of
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    66
        NONE => NONE
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    67
      | SOME m => SOME (m, the_default 1 (get_int props Markup.columnN)));
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    68
    fun property name = the_list (find_first (fn (x: string, _) => x = name) props);
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    69
  in (Pos (count, property Markup.fileN @ property Markup.idN)) end;
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    70
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    71
fun properties_of (Pos (count, props)) =
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    72
  (case count of
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    73
    NONE => []
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    74
  | 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
    75
26052
7d5b3e34a735 added default_properties;
wenzelm
parents: 26003
diff changeset
    76
fun default_properties default props =
7d5b3e34a735 added default_properties;
wenzelm
parents: 26003
diff changeset
    77
  if exists (member (op =) Markup.position_properties o #1) props then props
7d5b3e34a735 added default_properties;
wenzelm
parents: 26003
diff changeset
    78
  else properties_of default @ props;
7d5b3e34a735 added default_properties;
wenzelm
parents: 26003
diff changeset
    79
25817
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
    80
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    81
(* str_of *)
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    82
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    83
fun str_of pos =
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    84
  let
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    85
    val props = properties_of pos;
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    86
    val s =
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    87
      (case (line_of pos, file_of pos) of
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    88
        (SOME m, NONE) => "(line " ^ string_of_int m ^ ")"
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    89
      | (SOME m, SOME name) => "(line " ^ string_of_int m ^ " of " ^ quote name ^ ")"
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    90
      | _ => "");
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    91
  in
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    92
    if null props then ""
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    93
    else (if s = "" then "" else " ") ^ Markup.markup (Markup.properties props Markup.position) s
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    94
  end;
25817
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
    95
23627
f543538866a2 added property conversions;
wenzelm
parents: 22158
diff changeset
    96
25817
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
    97
(* thread data *)
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
    98
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
    99
local val tag = Universal.tag () : T Universal.tag in
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
   100
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
   101
fun thread_data () = the_default none (Multithreading.get_data tag);
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
   102
fun setmp_thread_data pos = Library.setmp_thread_data tag (thread_data ()) pos;
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
   103
25954
682e84b60e5c added setmp_thread_data_seq;
wenzelm
parents: 25817
diff changeset
   104
fun setmp_thread_data_seq pos f seq =
682e84b60e5c added setmp_thread_data_seq;
wenzelm
parents: 25817
diff changeset
   105
  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
   106
25817
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
   107
end;
23673
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
   108
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
   109
end;