src/Pure/PIDE/headless.scala
changeset 70801 5352449209b1
parent 70800 44eeca528557
child 70872 7c77fb7a6fc9
equal deleted inserted replaced
70800:44eeca528557 70801:5352449209b1
   269           else {
   269           else {
   270             val depth = dep_graph.node_depth(Load_State.count_file)
   270             val depth = dep_graph.node_depth(Load_State.count_file)
   271             maximals.sortBy(node => - depth(node))
   271             maximals.sortBy(node => - depth(node))
   272           }
   272           }
   273         val load_limit =
   273         val load_limit =
   274           if (commit.isDefined) session_options.int("headless_load_limit").toLong * 1024 * 1024
   274           if (commit.isDefined) (session_options.real("headless_load_limit") * 1024 * 1024).round
   275           else 0
   275           else 0
   276         val load_state = Load_State(Nil, rest, load_limit)
   276         val load_state = Load_State(Nil, rest, load_limit)
   277 
   277 
   278         Synchronized(Use_Theories_State(dep_graph, load_state, watchdog_timeout, commit))
   278         Synchronized(Use_Theories_State(dep_graph, load_state, watchdog_timeout, commit))
   279       }
   279       }