src/Tools/Code/code_namespace.ML
changeset 55293 42cf5802d36a
parent 55292 1e973b665b98
child 55605 b1b363e81c87
     1.1 --- a/src/Tools/Code/code_namespace.ML	Mon Feb 03 08:23:20 2014 +0100
     1.2 +++ b/src/Tools/Code/code_namespace.ML	Mon Feb 03 08:23:21 2014 +0100
     1.3 @@ -69,12 +69,16 @@
     1.4      | SOME prefix_name => if null force_module then prefix_name
     1.5          else (force_module, snd prefix_name);
     1.6  
     1.7 +fun has_priority identifiers = is_some o Code_Symbol.lookup identifiers;
     1.8 +
     1.9  fun build_proto_program { empty, add_stmt, add_dep } program =
    1.10    empty
    1.11    |> Code_Symbol.Graph.fold (fn (sym, (stmt, _)) => add_stmt sym stmt) program
    1.12    |> Code_Symbol.Graph.fold (fn (sym, (_, (_, syms))) =>
    1.13        Code_Symbol.Graph.Keys.fold (add_dep sym) syms) program;
    1.14  
    1.15 +fun prioritize has_priority = uncurry append o List.partition has_priority;
    1.16 +
    1.17  
    1.18  (** flat program structure **)
    1.19  
    1.20 @@ -90,6 +94,7 @@
    1.21      val prep_sym = prep_symbol ctxt { module_namespace = module_namespace,
    1.22        force_module = Long_Name.explode module_name, identifiers = identifiers }
    1.23        #>> Long_Name.implode;
    1.24 +    val sym_priority = has_priority identifiers;
    1.25  
    1.26      (* distribute statements over hierarchy *)
    1.27      fun add_stmt sym stmt =
    1.28 @@ -117,7 +122,8 @@
    1.29          val gr' = (Code_Symbol.Graph.map_node sym o apfst) (K base') gr;
    1.30        in (gr', nsp') end;
    1.31      fun declarations gr = (gr, empty_nsp)
    1.32 -      |> fold (fn sym => declare sym (Code_Symbol.Graph.get_node gr sym)) (Code_Symbol.Graph.keys gr) 
    1.33 +      |> fold (fn sym => declare sym (Code_Symbol.Graph.get_node gr sym))
    1.34 +          (prioritize sym_priority (Code_Symbol.Graph.keys gr))
    1.35        |> fst
    1.36        |> (Code_Symbol.Graph.map o K o apsnd) modify_stmt;
    1.37      val flat_program = proto_program
    1.38 @@ -176,7 +182,8 @@
    1.39      val module_namespace = build_module_namespace ctxt { module_prefix = "",
    1.40        module_name = module_name, identifiers = identifiers, reserved = reserved } program;
    1.41      val prep_sym = prep_symbol ctxt { module_namespace = module_namespace,
    1.42 -      force_module = Long_Name.explode module_name, identifiers = identifiers };
    1.43 +      force_module = Long_Name.explode module_name, identifiers = identifiers }
    1.44 +    val sym_priority = has_priority identifiers;
    1.45  
    1.46      (* building empty module hierarchy *)
    1.47      val empty_module = (empty_data, Code_Symbol.Graph.empty);
    1.48 @@ -223,9 +230,12 @@
    1.49      (* name declarations, data and statement modifications *)
    1.50      fun make_declarations nsps (data, nodes) =
    1.51        let
    1.52 -        val (module_fragments, stmt_syms) = List.partition
    1.53 -          (fn sym => case Code_Symbol.Graph.get_node nodes sym
    1.54 -            of (_, Module _) => true | _ => false) (Code_Symbol.Graph.keys nodes);
    1.55 +        val (module_fragments, stmt_syms) =
    1.56 +          Code_Symbol.Graph.keys nodes
    1.57 +          |> List.partition
    1.58 +              (fn sym => case Code_Symbol.Graph.get_node nodes sym
    1.59 +                of (_, Module _) => true | _ => false)
    1.60 +          |> pairself (prioritize sym_priority)
    1.61          fun declare namify sym (nsps, nodes) =
    1.62            let
    1.63              val (base, node) = Code_Symbol.Graph.get_node nodes sym;