src/Pure/ML/exn_properties_polyml.ML
author wenzelm
Tue, 08 Sep 2015 21:49:21 +0200
changeset 61138 dcbec1b22b07
parent 58714 ca0b7d7cc9a3
permissions -rw-r--r--
proper Windows path, notably for ML basis;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
50911
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML/exn_properties_polyml.ML
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
     3
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
     4
Exception properties for Poly/ML.
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
     5
*)
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
     6
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
     7
signature EXN_PROPERTIES =
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
     8
sig
56303
4cc3f4db3447 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents: 50911
diff changeset
     9
  val position_of: PolyML.location -> Position.T
50911
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
    10
  val get: exn -> Properties.T
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
    11
  val update: Properties.entry list -> exn -> exn
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
    12
end;
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
    13
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
    14
structure Exn_Properties: EXN_PROPERTIES =
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
    15
struct
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
    16
56303
4cc3f4db3447 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents: 50911
diff changeset
    17
(* source locations *)
4cc3f4db3447 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents: 50911
diff changeset
    18
4cc3f4db3447 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents: 50911
diff changeset
    19
fun props_of (loc: PolyML.location) =
50911
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
    20
  (case YXML.parse_body (#file loc) of
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
    21
    [] => []
58714
ca0b7d7cc9a3 suppress special Poly/ML location inBasis (see $ML_SOURCES/mlsource/MLCompiler/STRUCT_VALS.ML);
wenzelm
parents: 56303
diff changeset
    22
  | [XML.Text file] =>
ca0b7d7cc9a3 suppress special Poly/ML location inBasis (see $ML_SOURCES/mlsource/MLCompiler/STRUCT_VALS.ML);
wenzelm
parents: 56303
diff changeset
    23
      if file = "Standard Basis" then []
61138
dcbec1b22b07 proper Windows path, notably for ML basis;
wenzelm
parents: 58714
diff changeset
    24
      else [(Markup.fileN, ml_standard_path file)]
50911
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
    25
  | body => XML.Decode.properties body);
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
    26
56303
4cc3f4db3447 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents: 50911
diff changeset
    27
fun position_of loc =
4cc3f4db3447 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents: 50911
diff changeset
    28
  Position.make
4cc3f4db3447 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents: 50911
diff changeset
    29
   {line = #startLine loc,
4cc3f4db3447 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents: 50911
diff changeset
    30
    offset = #startPosition loc,
4cc3f4db3447 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents: 50911
diff changeset
    31
    end_offset = #endPosition loc,
4cc3f4db3447 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents: 50911
diff changeset
    32
    props = props_of loc};
4cc3f4db3447 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents: 50911
diff changeset
    33
4cc3f4db3447 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents: 50911
diff changeset
    34
4cc3f4db3447 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents: 50911
diff changeset
    35
(* exception properties *)
4cc3f4db3447 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents: 50911
diff changeset
    36
50911
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
    37
fun get exn =
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
    38
  (case PolyML.exceptionLocation exn of
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
    39
    NONE => []
56303
4cc3f4db3447 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents: 50911
diff changeset
    40
  | SOME loc => props_of loc);
50911
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
    41
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
    42
fun update entries exn =
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
    43
  let
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
    44
    val loc =
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
    45
      the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0}
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
    46
        (PolyML.exceptionLocation exn);
56303
4cc3f4db3447 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents: 50911
diff changeset
    47
    val props = props_of loc;
50911
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
    48
    val props' = fold Properties.put entries props;
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
    49
  in
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
    50
    if props = props' then exn
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
    51
    else
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
    52
      let
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
    53
        val loc' =
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
    54
          {file = YXML.string_of_body (XML.Encode.properties props'),
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
    55
            startLine = #startLine loc, endLine = #endLine loc,
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
    56
            startPosition = #startPosition loc, endPosition = #endPosition loc};
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
    57
      in
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
    58
        uninterruptible (fn _ => fn () => PolyML.raiseWithLocation (exn, loc')) ()
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
    59
          handle exn' => exn'
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
    60
      end
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
    61
  end;
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
    62
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
    63
end;
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff changeset
    64