diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp
index 247fbac12dd..aa4fd641681 100644
--- a/src/goto-cc/compile.cpp
+++ b/src/goto-cc/compile.cpp
@@ -34,6 +34,7 @@ Date: June 2006
 #include <goto-programs/read_goto_binary.h>
 #include <goto-programs/write_goto_binary.h>
 
+#include <langapi/language_file.h>
 #include <langapi/mode.h>
 
 #include <linking/static_lifetime_init.h>
@@ -75,22 +76,20 @@ Date: June 2006
 /// \return true on error, false otherwise
 bool compilet::doit()
 {
-  compiled_functions.clear();
+  goto_model.goto_functions.clear();
 
   add_compiler_specific_defines(config);
 
   // Parse command line for source and object file names
-  for(std::size_t i=0; i<_cmdline.args.size(); i++)
-    if(add_input_file(_cmdline.args[i]))
+  for(const auto &arg : cmdline.args)
+    if(add_input_file(arg))
       return true;
 
-  for(std::list<std::string>::const_iterator it = libraries.begin();
-      it!=libraries.end();
-      it++)
+  for(const auto &library : libraries)
   {
-    if(!find_library(*it))
+    if(!find_library(library))
       // GCC is going to complain if this doesn't exist
-      debug() << "Library not found: " << *it << " (ignoring)" << eom;
+      debug() << "Library not found: " << library << " (ignoring)" << eom;
   }
 
   statistics() << "No. of source files: " << source_files.size() << eom;
@@ -307,15 +306,12 @@ bool compilet::find_library(const std::string &name)
 {
   std::string tmp;
 
-  for(std::list<std::string>::const_iterator
-      it=library_paths.begin();
-      it!=library_paths.end();
-      it++)
+  for(const auto &library_path : library_paths)
   {
     #ifdef _WIN32
-    tmp = *it + "\\lib";
+    tmp = library_path + "\\lib";
     #else
-    tmp = *it + "/lib";
+    tmp = library_path + "/lib";
     #endif
 
     std::ifstream in(tmp+name+".a");
@@ -350,13 +346,12 @@ bool compilet::link()
 {
   // "compile" hitherto uncompiled functions
   statistics() << "Compiling functions" << eom;
-  convert_symbols(compiled_functions);
+  convert_symbols(goto_model.goto_functions);
 
   // parse object files
   for(const auto &file_name : object_files)
   {
-    if(read_object_and_link(file_name, symbol_table,
-                            compiled_functions, get_message_handler()))
+    if(read_object_and_link(file_name, goto_model, get_message_handler()))
       return true;
   }
 
@@ -367,23 +362,23 @@ bool compilet::link()
     // new symbols may have been added to a previously linked file
     // make sure a new entry point is created that contains all
     // static initializers
-    compiled_functions.function_map.erase(INITIALIZE_FUNCTION);
+    goto_model.goto_functions.function_map.erase(INITIALIZE_FUNCTION);
 
-    symbol_table.remove(goto_functionst::entry_point());
-    compiled_functions.function_map.erase(goto_functionst::entry_point());
+    goto_model.symbol_table.remove(goto_functionst::entry_point());
+    goto_model.goto_functions.function_map.erase(
+      goto_functionst::entry_point());
 
-    if(ansi_c_entry_point(symbol_table, get_message_handler()))
+    if(ansi_c_entry_point(goto_model.symbol_table, get_message_handler()))
       return true;
 
     // entry_point may (should) add some more functions.
-    convert_symbols(compiled_functions);
+    convert_symbols(goto_model.goto_functions);
   }
 
-  if(write_object_file(
-      output_file_executable, symbol_table, compiled_functions))
+  if(write_object_file(output_file_executable, goto_model))
     return true;
 
-  return add_written_cprover_symbols(symbol_table);
+  return add_written_cprover_symbols(goto_model.symbol_table);
 }
 
 /// parses source files and writes object files, or keeps the symbols in the
@@ -423,7 +418,7 @@ bool compilet::compile()
       // output an object file for every source file
 
       // "compile" functions
-      convert_symbols(compiled_functions);
+      convert_symbols(goto_model.goto_functions);
 
       std::string cfn;
 
@@ -440,14 +435,13 @@ bool compilet::compile()
       else
         cfn = output_file_object;
 
-      if(write_object_file(cfn, symbol_table, compiled_functions))
+      if(write_object_file(cfn, goto_model))
         return true;
 
-      if(add_written_cprover_symbols(symbol_table))
+      if(add_written_cprover_symbols(goto_model.symbol_table))
         return true;
 
-      symbol_table.clear(); // clean symbol table for next source file.
-      compiled_functions.clear();
+      goto_model.clear(); // clean symbol table for next source file.
     }
   }
 
@@ -456,7 +450,9 @@ bool compilet::compile()
 
 /// parses a source file (low-level parsing)
 /// \return true on error, false otherwise
-bool compilet::parse(const std::string &file_name)
+bool compilet::parse(
+  const std::string &file_name,
+  language_filest &language_files)
 {
   if(file_name=="-")
     return parse_stdin();
@@ -527,8 +523,7 @@ bool compilet::parse(const std::string &file_name)
 
     if(lf.language->parse(infile, file_name))
     {
-      if(get_ui()==ui_message_handlert::uit::PLAIN)
-        error() << "PARSING ERROR" << eom;
+      error() << "PARSING ERROR" << eom;
       return true;
     }
   }
@@ -571,8 +566,7 @@ bool compilet::parse_stdin()
   {
     if(language.parse(std::cin, ""))
     {
-      if(get_ui()==ui_message_handlert::uit::PLAIN)
-        error() << "PARSING ERROR" << eom;
+      error() << "PARSING ERROR" << eom;
       return true;
     }
   }
@@ -586,10 +580,9 @@ bool compilet::parse_stdin()
 /// \return true on error, false otherwise
 bool compilet::write_object_file(
   const std::string &file_name,
-  const symbol_tablet &lsymbol_table,
-  goto_functionst &functions)
+  const goto_modelt &goto_model)
 {
-  return write_bin_object_file(file_name, lsymbol_table, functions);
+  return write_bin_object_file(file_name, goto_model);
 }
 
 /// writes the goto functions in the function table to a binary format object
@@ -598,15 +591,14 @@ bool compilet::write_object_file(
 /// \return true on error, false otherwise
 bool compilet::write_bin_object_file(
   const std::string &file_name,
-  const symbol_tablet &lsymbol_table,
-  goto_functionst &functions)
+  const goto_modelt &goto_model)
 {
   statistics() << "Writing binary format object `"
                << file_name << "'" << eom;
 
   // symbols
-  statistics() << "Symbols in table: "
-               << lsymbol_table.symbols.size() << eom;
+  statistics() << "Symbols in table: " << goto_model.symbol_table.symbols.size()
+               << eom;
 
   std::ofstream outfile(file_name, std::ios::binary);
 
@@ -616,12 +608,12 @@ bool compilet::write_bin_object_file(
     return true;
   }
 
-  if(write_goto_binary(outfile, lsymbol_table, functions))
+  if(write_goto_binary(outfile, goto_model))
     return true;
 
-  unsigned cnt=function_body_count(functions);
+  const auto cnt = function_body_count(goto_model.goto_functions);
 
-  statistics() << "Functions: " << functions.function_map.size()
+  statistics() << "Functions: " << goto_model.goto_functions.function_map.size()
                << "; " << cnt << " have a body." << eom;
 
   outfile.close();
@@ -634,29 +626,35 @@ bool compilet::write_bin_object_file(
 /// \return true on error, false otherwise
 bool compilet::parse_source(const std::string &file_name)
 {
-  if(parse(file_name))
+  language_filest language_files;
+  language_files.set_message_handler(get_message_handler());
+
+  if(parse(file_name, language_files))
     return true;
 
-  if(typecheck()) // we just want to typecheck this one file here
+  // we just typecheck one file here
+  if(language_files.typecheck(goto_model.symbol_table))
+  {
+    error() << "CONVERSION ERROR" << eom;
     return true;
+  }
 
-  if((has_suffix(file_name, ".class") ||
-      has_suffix(file_name, ".jar")) &&
-     final())
+  if(language_files.final(goto_model.symbol_table))
+  {
+    error() << "CONVERSION ERROR" << eom;
     return true;
+  }
 
-  // so we remove it from the list afterwards
-  language_files.remove_file(file_name);
   return false;
 }
 
 /// constructor
 /// \return nothing
-compilet::compilet(cmdlinet &_cmdline, ui_message_handlert &mh, bool Werror):
-  language_uit(_cmdline, mh),
-  ns(symbol_table),
-  cmdline(_cmdline),
-  warning_is_fatal(Werror)
+compilet::compilet(cmdlinet &_cmdline, message_handlert &mh, bool Werror)
+  : messaget(mh),
+    ns(goto_model.symbol_table),
+    cmdline(_cmdline),
+    warning_is_fatal(Werror)
 {
   mode=COMPILE_LINK_EXECUTABLE;
   echo_file_name=false;
@@ -670,24 +668,20 @@ compilet::~compilet()
 {
   // clean up temp dirs
 
-  for(std::list<std::string>::const_iterator it = tmp_dirs.begin();
-      it!=tmp_dirs.end();
-      it++)
-    delete_directory(*it);
+  for(const auto &dir : tmp_dirs)
+    delete_directory(dir);
 }
 
-unsigned compilet::function_body_count(const goto_functionst &functions) const
+std::size_t
+compilet::function_body_count(const goto_functionst &functions) const
 {
-  int fbs=0;
+  std::size_t count = 0;
 
-  for(goto_functionst::function_mapt::const_iterator it=
-      functions.function_map.begin();
-      it != functions.function_map.end();
-      it++)
-    if(it->second.body_available())
-      fbs++;
+  for(const auto &f : functions.function_map)
+    if(f.second.body_available())
+      count++;
 
-  return fbs;
+  return count;
 }
 
 void compilet::add_compiler_specific_defines(configt &config) const
@@ -698,31 +692,29 @@ void compilet::add_compiler_specific_defines(configt &config) const
 
 void compilet::convert_symbols(goto_functionst &dest)
 {
-  goto_convert_functionst converter(symbol_table, get_message_handler());
+  goto_convert_functionst converter(
+    goto_model.symbol_table, get_message_handler());
 
   // the compilation may add symbols!
 
   symbol_tablet::symbolst::size_type before=0;
 
-  while(before!=symbol_table.symbols.size())
+  while(before != goto_model.symbol_table.symbols.size())
   {
-    before=symbol_table.symbols.size();
+    before = goto_model.symbol_table.symbols.size();
 
     typedef std::set<irep_idt> symbols_sett;
     symbols_sett symbols;
 
-    for(const auto &named_symbol : symbol_table.symbols)
+    for(const auto &named_symbol : goto_model.symbol_table.symbols)
       symbols.insert(named_symbol.first);
 
     // the symbol table iterators aren't stable
-    for(symbols_sett::const_iterator
-        it=symbols.begin();
-        it!=symbols.end();
-        ++it)
+    for(const auto &symbol : symbols)
     {
-      symbol_tablet::symbolst::const_iterator s_it=
-        symbol_table.symbols.find(*it);
-      assert(s_it!=symbol_table.symbols.end());
+      symbol_tablet::symbolst::const_iterator s_it =
+        goto_model.symbol_table.symbols.find(symbol);
+      CHECK_RETURN(s_it != goto_model.symbol_table.symbols.end());
 
       if(
         s_it->second.is_function() && !s_it->second.is_compiled() &&
@@ -730,7 +722,7 @@ void compilet::convert_symbols(goto_functionst &dest)
       {
         debug() << "Compiling " << s_it->first << eom;
         converter.convert_function(s_it->first, dest.function_map[s_it->first]);
-        symbol_table.get_writeable_ref(*it).set_compiled();
+        goto_model.symbol_table.get_writeable_ref(symbol).set_compiled();
       }
     }
   }
diff --git a/src/goto-cc/compile.h b/src/goto-cc/compile.h
index cc2295ea8ea..a423e356cfb 100644
--- a/src/goto-cc/compile.h
+++ b/src/goto-cc/compile.h
@@ -14,17 +14,22 @@ Date: June 2006
 #ifndef CPROVER_GOTO_CC_COMPILE_H
 #define CPROVER_GOTO_CC_COMPILE_H
 
-#include <util/symbol.h>
+#include <util/cmdline.h>
+#include <util/message.h>
 #include <util/rename_symbol.h>
 
-#include <langapi/language_ui.h>
 #include <goto-programs/goto_model.h>
 
-class compilet:public language_uit
+class language_filest;
+
+class compilet : public messaget
 {
 public:
+  // compilation results
   namespacet ns;
-  goto_functionst compiled_functions;
+  goto_modelt goto_model;
+
+  // configuration
   bool echo_file_name;
   std::string working_directory;
   std::string override_language;
@@ -50,7 +55,7 @@ class compilet:public language_uit
   // the two options below are mutually exclusive -- use either or
   std::string output_file_object, output_directory_object;
 
-  compilet(cmdlinet &_cmdline, ui_message_handlert &mh, bool Werror);
+  compilet(cmdlinet &_cmdline, message_handlert &mh, bool Werror);
 
   ~compilet();
 
@@ -58,7 +63,7 @@ class compilet:public language_uit
   bool find_library(const std::string &);
   bool add_files_from_archive(const std::string &file_name, bool thin_archive);
 
-  bool parse(const std::string &filename);
+  bool parse(const std::string &filename, language_filest &);
   bool parse_stdin();
   bool doit();
   bool compile();
@@ -66,15 +71,9 @@ class compilet:public language_uit
 
   bool parse_source(const std::string &);
 
-  bool write_object_file(
-    const std::string &,
-    const symbol_tablet &,
-    goto_functionst &);
+  bool write_object_file(const std::string &, const goto_modelt &);
 
-  bool write_bin_object_file(
-    const std::string &,
-    const symbol_tablet &,
-    goto_functionst &);
+  bool write_bin_object_file(const std::string &, const goto_modelt &);
 
   /// \brief Has this compiler written any object files?
   bool wrote_object_files() const { return wrote_object; }
@@ -97,7 +96,7 @@ class compilet:public language_uit
   cmdlinet &cmdline;
   bool warning_is_fatal;
 
-  unsigned function_body_count(const goto_functionst &) const;
+  std::size_t function_body_count(const goto_functionst &) const;
 
   void add_compiler_specific_defines(class configt &config) const;
 
diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp
index b2fbb0cdfe7..08b72950982 100644
--- a/src/goto-cc/linker_script_merge.cpp
+++ b/src/goto-cc/linker_script_merge.cpp
@@ -32,12 +32,11 @@ int linker_script_merget::add_linker_script_definitions()
 
   temporary_filet linker_def_outfile("goto-cc-linker-info", ".json");
   std::list<irep_idt> linker_defined_symbols;
-  int fail=
-    get_linker_script_data(
-      linker_defined_symbols,
-      compiler.symbol_table,
-      elf_binary,
-      linker_def_outfile());
+  int fail = get_linker_script_data(
+    linker_defined_symbols,
+    compiler.goto_model.symbol_table,
+    elf_binary,
+    linker_def_outfile());
   // ignore linker script parsing failures until the code is tested more widely
   if(fail!=0)
     return 0;
@@ -58,11 +57,10 @@ int linker_script_merget::add_linker_script_definitions()
     return fail;
   }
 
-  symbol_tablet original_st;
-  goto_functionst original_gf;
+  goto_modelt original_goto_model;
 
-  fail=read_goto_binary(goto_binary, original_st, original_gf,
-      get_message_handler());
+  fail =
+    read_goto_binary(goto_binary, original_goto_model, get_message_handler());
 
   if(fail!=0)
   {
@@ -72,19 +70,20 @@ int linker_script_merget::add_linker_script_definitions()
 
   fail=1;
   linker_valuest linker_values;
-  const auto &pair=original_gf.function_map.find(INITIALIZE_FUNCTION);
-  if(pair==original_gf.function_map.end())
+  const auto &pair =
+    original_goto_model.goto_functions.function_map.find(INITIALIZE_FUNCTION);
+  if(pair == original_goto_model.goto_functions.function_map.end())
   {
     error() << "No " << INITIALIZE_FUNCTION << " found in goto_functions"
             << eom;
     return fail;
   }
-  fail=ls_data2instructions(
-      data,
-      cmdline.get_value('T'),
-      pair->second.body,
-      original_st,
-      linker_values);
+  fail = ls_data2instructions(
+    data,
+    cmdline.get_value('T'),
+    pair->second.body,
+    original_goto_model.symbol_table,
+    linker_values);
   if(fail!=0)
   {
     error() << "Could not add linkerscript defs to " INITIALIZE_FUNCTION << eom;
@@ -98,8 +97,7 @@ int linker_script_merget::add_linker_script_definitions()
   // The keys of linker_values are exactly the elements of
   // linker_defined_symbols, so iterate over linker_values from now on.
 
-  fail=pointerize_linker_defined_symbols(original_gf, original_st,
-      linker_values);
+  fail = pointerize_linker_defined_symbols(original_goto_model, linker_values);
 
   if(fail!=0)
   {
@@ -107,7 +105,7 @@ int linker_script_merget::add_linker_script_definitions()
     return fail;
   }
 
-  fail=compiler.write_object_file(goto_binary, original_st, original_gf);
+  fail = compiler.write_object_file(goto_binary, original_goto_model);
 
   if(fail!=0)
     error() << "Could not write linkerscript-augmented binary" << eom;
@@ -185,17 +183,16 @@ linker_script_merget::linker_script_merget(
 {}
 
 int linker_script_merget::pointerize_linker_defined_symbols(
-      goto_functionst &goto_functions,
-      symbol_tablet &symbol_table,
-      const linker_valuest &linker_values)
+  goto_modelt &goto_model,
+  const linker_valuest &linker_values)
 {
-  const namespacet ns(symbol_table);
+  const namespacet ns(goto_model.symbol_table);
 
   int ret=0;
   // First, pointerize the actual linker-defined symbols
   for(const auto &pair : linker_values)
   {
-    const auto maybe_symbol=symbol_table.get_writeable(pair.first);
+    const auto maybe_symbol = goto_model.symbol_table.get_writeable(pair.first);
     if(!maybe_symbol)
       continue;
     symbolt &entry=*maybe_symbol;
@@ -206,7 +203,7 @@ int linker_script_merget::pointerize_linker_defined_symbols(
 
   // Next, find all occurrences of linker-defined symbols that are _values_
   // of some symbol in the symbol table, and pointerize them too
-  for(const auto &pair : symbol_table.symbols)
+  for(const auto &pair : goto_model.symbol_table.symbols)
   {
     std::list<symbol_exprt> to_pointerize;
     symbols_to_pointerize(linker_values, pair.second.value, to_pointerize);
@@ -215,8 +212,8 @@ int linker_script_merget::pointerize_linker_defined_symbols(
       continue;
     debug() << "Pointerizing the symbol-table value of symbol " << pair.first
             << eom;
-    int fail=pointerize_subexprs_of(
-      symbol_table.get_writeable_ref(pair.first).value,
+    int fail = pointerize_subexprs_of(
+      goto_model.symbol_table.get_writeable_ref(pair.first).value,
       to_pointerize,
       linker_values,
       ns);
@@ -232,7 +229,7 @@ int linker_script_merget::pointerize_linker_defined_symbols(
 
   // Finally, pointerize all occurrences of linker-defined symbols in the
   // goto program
-  for(auto &gf : goto_functions.function_map)
+  for(auto &gf : goto_model.goto_functions.function_map)
   {
     goto_programt &program=gf.second.body;
     Forall_goto_program_instructions(iit, program)
diff --git a/src/goto-cc/linker_script_merge.h b/src/goto-cc/linker_script_merge.h
index e260247387f..64000245d26 100644
--- a/src/goto-cc/linker_script_merge.h
+++ b/src/goto-cc/linker_script_merge.h
@@ -156,10 +156,7 @@ class linker_script_merget:public messaget
   /// \post Expressions of the shape `&foo[0]`, `&foo`, and `foo`, where `foo`
   ///       is a linker-script defined symbol with type array, have been
   ///       converted to `foo` whose type is `char*`.
-  int pointerize_linker_defined_symbols(
-      goto_functionst &goto_functions,
-      symbol_tablet &symbol_table,
-      const linker_valuest &linker_values);
+  int pointerize_linker_defined_symbols(goto_modelt &, const linker_valuest &);
 
   /// \param expr an expr whose subexpressions may need to be pointerized
   /// \param to_pointerize  The symbols that are contained in the subexpressions
diff --git a/src/goto-programs/initialize_goto_model.cpp b/src/goto-programs/initialize_goto_model.cpp
index 564a0a1eaad..73cc28ac366 100644
--- a/src/goto-programs/initialize_goto_model.cpp
+++ b/src/goto-programs/initialize_goto_model.cpp
@@ -18,7 +18,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/unicode.h>
 
 #include <langapi/mode.h>
-#include <langapi/language_ui.h>
 #include <langapi/language.h>
 
 #include <goto-programs/rebuild_goto_start_function.h>
diff --git a/src/util/cout_message.h b/src/util/cout_message.h
index 4972a73bbb0..913de68fd2c 100644
--- a/src/util/cout_message.h
+++ b/src/util/cout_message.h
@@ -10,7 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_UTIL_COUT_MESSAGE_H
 #define CPROVER_UTIL_COUT_MESSAGE_H
 
-#include "ui_message.h"
+#include "message.h"
 
 class cout_message_handlert:public stream_message_handlert
 {
@@ -26,7 +26,7 @@ class cerr_message_handlert:public stream_message_handlert
   cerr_message_handlert();
 };
 
-class console_message_handlert:public ui_message_handlert
+class console_message_handlert : public message_handlert
 {
 public:
   // level 4 and upwards go to cout, level 1-3 to cerr
@@ -49,7 +49,7 @@ class console_message_handlert:public ui_message_handlert
   const bool always_flush;
 };
 
-class gcc_message_handlert:public ui_message_handlert
+class gcc_message_handlert : public message_handlert
 {
 public:
   // aims to imitate the messages gcc prints