additional ML parse tree components for Poly/ML 5.5.3, or later;
authorwenzelm
Thu Jul 16 14:40:23 2015 +0200 (2015-07-16)
changeset 607314ac4b314d93c
parent 60730 02c2860fcf30
child 60732 18299765542e
additional ML parse tree components for Poly/ML 5.5.3, or later;
support for ML completion;
tuned;
src/Pure/General/completion.ML
src/Pure/ML-Systems/ml_parse_tree.ML
src/Pure/ML-Systems/ml_parse_tree_polyml-5.5.3.ML
src/Pure/ML-Systems/polyml.ML
src/Pure/ML/ml_compiler_polyml.ML
src/Pure/ROOT
     1.1 --- a/src/Pure/General/completion.ML	Thu Jul 16 11:38:18 2015 +0200
     1.2 +++ b/src/Pure/General/completion.ML	Thu Jul 16 14:40:23 2015 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4    val names: Position.T -> (string * (string * string)) list -> T
     1.5    val none: T
     1.6    val make: string * Position.T -> ((string -> bool) -> (string * (string * string)) list) -> T
     1.7 +  val encode: T -> XML.body
     1.8    val reported_text: T -> string
     1.9    val suppress_abbrevs: string -> Markup.T list
    1.10  end;
    1.11 @@ -40,14 +41,18 @@
    1.12    then names pos (make_names (String.isPrefix (Name.clean name)))
    1.13    else none;
    1.14  
    1.15 +fun encode completion =
    1.16 +  let
    1.17 +    val {total, names, ...} = dest completion;
    1.18 +    open XML.Encode;
    1.19 +  in pair int (list (pair string (pair string string))) (total, names) end;
    1.20 +
    1.21  fun reported_text completion =
    1.22 -  let val {pos, total, names} = dest completion in
    1.23 +  let val {pos, names, ...} = dest completion in
    1.24      if Position.is_reported pos andalso not (null names) then
    1.25        let
    1.26          val markup = Position.markup pos Markup.completion;
    1.27 -        val body = (total, names) |>
    1.28 -          let open XML.Encode in pair int (list (pair string (pair string string))) end;
    1.29 -      in YXML.string_of (XML.Elem (markup, body)) end
    1.30 +      in YXML.string_of (XML.Elem (markup, encode completion)) end
    1.31      else ""
    1.32    end;
    1.33  
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/ML-Systems/ml_parse_tree.ML	Thu Jul 16 14:40:23 2015 +0200
     2.3 @@ -0,0 +1,19 @@
     2.4 +(*  Title:      Pure/ML/ml_parse_tree.ML
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Additional ML parse tree components for Poly/ML.
     2.8 +*)
     2.9 +
    2.10 +signature ML_PARSE_TREE =
    2.11 +sig
    2.12 +  val completions: PolyML.ptProperties -> string list option
    2.13 +  val break_point: PolyML.ptProperties -> bool Unsynchronized.ref option
    2.14 +end;
    2.15 +
    2.16 +structure ML_Parse_Tree: ML_PARSE_TREE =
    2.17 +struct
    2.18 +
    2.19 +fun completions _ = NONE;
    2.20 +fun break_point _ = NONE;
    2.21 +
    2.22 +end;
    2.23 \ No newline at end of file
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/ML-Systems/ml_parse_tree_polyml-5.5.3.ML	Thu Jul 16 14:40:23 2015 +0200
     3.3 @@ -0,0 +1,16 @@
     3.4 +(*  Title:      Pure/ML/ml_parse_tree_polyml-5.5.3.ML
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Additional ML parse tree components for Poly/ML 5.5.3, or later.
     3.8 +*)
     3.9 +
    3.10 +structure ML_Parse_Tree: ML_PARSE_TREE =
    3.11 +struct
    3.12 +
    3.13 +fun completions (PolyML.PTcompletions x) = SOME x
    3.14 +  | completions _ = NONE;
    3.15 +
    3.16 +fun break_point (PolyML.PTbreakPoint x) = SOME x
    3.17 +  | break_point _ = NONE;
    3.18 +
    3.19 +end;
    3.20 \ No newline at end of file
     4.1 --- a/src/Pure/ML-Systems/polyml.ML	Thu Jul 16 11:38:18 2015 +0200
     4.2 +++ b/src/Pure/ML-Systems/polyml.ML	Thu Jul 16 14:40:23 2015 +0200
     4.3 @@ -132,6 +132,9 @@
     4.4  
     4.5  fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
     4.6  
     4.7 +use "ML-Systems/ml_parse_tree.ML";
     4.8 +if ML_System.name = "polyml-5.5.3" then use "ML-Systems/ml_parse_tree_polyml-5.5.3.ML" else ();
     4.9 +
    4.10  
    4.11  (* ML debugger *)
    4.12  
     5.1 --- a/src/Pure/ML/ml_compiler_polyml.ML	Thu Jul 16 11:38:18 2015 +0200
     5.2 +++ b/src/Pure/ML/ml_compiler_polyml.ML	Thu Jul 16 14:40:23 2015 +0200
     5.3 @@ -43,13 +43,26 @@
     5.4            in cons (pos, markup, fn () => "") end
     5.5        end;
     5.6  
     5.7 +    fun reported_completions loc names =
     5.8 +      let val pos = Exn_Properties.position_of loc in
     5.9 +        if is_reported pos then
    5.10 +          let
    5.11 +            val completion = Completion.names pos (map (fn a => (a, ("ML", ""))) names);
    5.12 +            val xml = Completion.encode completion;
    5.13 +          in cons (pos, fn () => Markup.completion, fn () => YXML.string_of_body xml) end
    5.14 +        else I
    5.15 +      end;
    5.16 +
    5.17      fun reported loc (PolyML.PTtype types) = reported_types loc types
    5.18        | reported loc (PolyML.PTdeclaredAt decl) = reported_entity Markup.ML_defN loc decl
    5.19        | reported loc (PolyML.PTopenedAt decl) = reported_entity Markup.ML_openN loc decl
    5.20        | reported loc (PolyML.PTstructureAt decl) = reported_entity Markup.ML_structureN loc decl
    5.21        | reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
    5.22        | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
    5.23 -      | reported _ _ = I
    5.24 +      | reported loc pt =
    5.25 +          (case ML_Parse_Tree.completions pt of
    5.26 +            SOME names => reported_completions loc names
    5.27 +          | NONE => I)
    5.28      and reported_tree (loc, props) = fold (reported loc) props;
    5.29  
    5.30      val persistent_reports = reported_tree parse_tree [];
     6.1 --- a/src/Pure/ROOT	Thu Jul 16 11:38:18 2015 +0200
     6.2 +++ b/src/Pure/ROOT	Thu Jul 16 14:40:23 2015 +0200
     6.3 @@ -9,20 +9,22 @@
     6.4      "ML-Systems/ml_debugger_dummy.ML"
     6.5      "ML-Systems/ml_debugger_polyml-5.5.3.ML"
     6.6      "ML-Systems/ml_name_space.ML"
     6.7 +    "ML-Systems/ml_parse_tree.ML"
     6.8 +    "ML-Systems/ml_parse_tree_polyml-5.5.3.ML"
     6.9      "ML-Systems/ml_positions.ML"
    6.10      "ML-Systems/ml_pretty.ML"
    6.11      "ML-Systems/ml_system.ML"
    6.12      "ML-Systems/multithreading.ML"
    6.13      "ML-Systems/multithreading_polyml.ML"
    6.14      "ML-Systems/overloading_smlnj.ML"
    6.15 -    "ML-Systems/polyml.ML"
    6.16      "ML-Systems/polyml-5.5.2.ML"
    6.17      "ML-Systems/polyml-5.5.3.ML"
    6.18 +    "ML-Systems/polyml.ML"
    6.19      "ML-Systems/pp_dummy.ML"
    6.20      "ML-Systems/proper_int.ML"
    6.21 +    "ML-Systems/share_common_data_polyml-5.3.0.ML"
    6.22      "ML-Systems/single_assignment.ML"
    6.23      "ML-Systems/single_assignment_polyml.ML"
    6.24 -    "ML-Systems/share_common_data_polyml-5.3.0.ML"
    6.25      "ML-Systems/smlnj.ML"
    6.26      "ML-Systems/thread_dummy.ML"
    6.27      "ML-Systems/universal.ML"
    6.28 @@ -35,18 +37,23 @@
    6.29      "General/exn.ML"
    6.30      "ML-Systems/compiler_polyml.ML"
    6.31      "ML-Systems/exn_trace_polyml-5.5.1.ML"
    6.32 +    "ML-Systems/ml_debugger_dummy.ML"
    6.33 +    "ML-Systems/ml_debugger_polyml-5.5.3.ML"
    6.34      "ML-Systems/ml_name_space.ML"
    6.35 +    "ML-Systems/ml_parse_tree.ML"
    6.36 +    "ML-Systems/ml_parse_tree_polyml-5.5.3.ML"
    6.37      "ML-Systems/ml_positions.ML"
    6.38      "ML-Systems/ml_pretty.ML"
    6.39      "ML-Systems/ml_system.ML"
    6.40      "ML-Systems/multithreading.ML"
    6.41      "ML-Systems/multithreading_polyml.ML"
    6.42      "ML-Systems/overloading_smlnj.ML"
    6.43 -    "ML-Systems/polyml.ML"
    6.44      "ML-Systems/polyml-5.5.2.ML"
    6.45      "ML-Systems/polyml-5.5.3.ML"
    6.46 +    "ML-Systems/polyml.ML"
    6.47      "ML-Systems/pp_dummy.ML"
    6.48      "ML-Systems/proper_int.ML"
    6.49 +    "ML-Systems/share_common_data_polyml-5.3.0.ML"
    6.50      "ML-Systems/single_assignment.ML"
    6.51      "ML-Systems/single_assignment_polyml.ML"
    6.52      "ML-Systems/smlnj.ML"